<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
<link href="common/css/sf.css" rel="stylesheet" type="text/css"/>
<title>UseAuto: Theory and Practice of Automation in Coq Proofs</title>
</head>
<link href="common/jquery-ui/jquery-ui.css" rel="stylesheet">
<script src="common/jquery-ui/external/jquery/jquery.js"></script>
<script src="common/jquery-ui/jquery-ui.js"></script>
<script src="common/toggleproofs.js"></script>
<link href="common/css/plf.css" rel="stylesheet" type="text/css"/>

<body>

<div id="page">

<div id="header">
<a href='https://www.cis.upenn.edu/~bcpierce/sf/current/index.html'>
<img src='common/media/image/sf_logo_sm.png'></a>
</br><a href='index.html'>  <span class='booktitleinheader'>Volume 2: Programming Language Foundations</span><br></br>
<ul id='menu'>
   <a href='toc.html'><li class='section_name'>Table of Contents</li></a>
   <a href='coqindex.html'><li class='section_name'>Index</li></a>
   <a href='deps.html'><li class='section_name'>Roadmap</li></a>
</ul>
</a></div>

<div id="main">

<h1 class="libtitle">UseAuto<span class="subtitle">Theory and Practice of Automation in Coq Proofs</span></h1>


<div class="code code-tight">
<span class="comment">(*&nbsp;Chapter&nbsp;written&nbsp;and&nbsp;maintained&nbsp;by&nbsp;Arthur&nbsp;Chargueraud&nbsp;*)</span><br/>
</div>

<div class="doc">
In a machine-checked proof, every single detail has to be
    justified.  This can result in huge proof scripts. Fortunately,
    Coq comes with a proof-search mechanism and with several decision
    procedures that enable the system to automatically synthesize
    simple pieces of proof. Automation is very powerful when set up
    appropriately. The purpose of this chapter is to explain the
    basics of how automation works in Coq.

<div class="paragraph"> </div>

    The chapter is organized in two parts. The first part focuses on a
    general mechanism called "proof search." In short, proof search
    consists in naively trying to apply lemmas and assumptions in all
    possible ways. The second part describes "decision procedures",
    which are tactics that are very good at solving proof obligations
    that fall in some particular fragments of the logic of Coq.

<div class="paragraph"> </div>

    Many of the examples used in this chapter consist of small lemmas
    that have been made up to illustrate particular aspects of automation.
    These examples are completely independent from the rest of the Software
    Foundations course. This chapter also contains some bigger examples
    which are used to explain how to use automation in realistic proofs.
    These examples are taken from other chapters of the course (mostly
    from STLC), and the proofs that we present make use of the tactics
    from the library <span class="inlinecode"><span class="id" type="var">LibTactics.v</span></span>, which is presented in the chapter
    <span class="inlinecode"><span class="id" type="var">UseTactics</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="var">From</span> <span class="id" type="var">Coq</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Arith.Arith</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="var">From</span> <span class="id" type="var">PLF</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Maps</span>.<br/>
<span class="id" type="var">From</span> <span class="id" type="var">PLF</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Smallstep</span>.<br/>
<span class="id" type="var">From</span> <span class="id" type="var">PLF</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Stlc</span>.<br/>
<span class="id" type="var">From</span> <span class="id" type="var">PLF</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">LibTactics</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="var">From</span> <span class="id" type="var">PLF</span> <span class="id" type="keyword">Require</span> <span class="id" type="var">Imp</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="var">From</span> <span class="id" type="var">Coq</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Lists.List</span>.<br/>
<span class="id" type="keyword">Import</span> <span class="id" type="var">ListNotations</span>.<br/>
</div>

<div class="doc">
<a name="lab545"></a><h1 class="section">Basic Features of Proof Search</h1>

<div class="paragraph"> </div>

 The idea of proof search is to replace a sequence of tactics
    applying lemmas and assumptions with a call to a single tactic,
    for example <span class="inlinecode"><span class="id" type="tactic">auto</span></span>. This form of proof automation saves a lot of
    effort. It typically leads to much shorter proof scripts, and to
    scripts that are typically more robust to change.  If one makes a
    little change to a definition, a proof that exploits automation
    probably won't need to be modified at all. Of course, using too
    much automation is a bad idea.  When a proof script no longer
    records the main arguments of a proof, it becomes difficult to fix
    it when it gets broken after a change in a definition. Overall, a
    reasonable use of automation is generally a big win, as it saves a
    lot of time both in building proof scripts and in subsequently
    maintaining those proof scripts. 
</div>

<div class="doc">
<a name="lab546"></a><h2 class="section">Strength of Proof Search</h2>

<div class="paragraph"> </div>

 We are going to study four proof-search tactics: <span class="inlinecode"><span class="id" type="tactic">auto</span></span>, <span class="inlinecode"><span class="id" type="tactic">eauto</span></span>,
    <span class="inlinecode"><span class="id" type="var">iauto</span></span> and <span class="inlinecode"><span class="id" type="var">jauto</span></span>. The tactics <span class="inlinecode"><span class="id" type="tactic">auto</span></span> and <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> are builtin
    in Coq. The tactic <span class="inlinecode"><span class="id" type="var">iauto</span></span> is a shorthand for the builtin tactic
    <span class="inlinecode"><span class="id" type="tactic">try</span></span> <span class="inlinecode"><span class="id" type="var">solve</span></span> <span class="inlinecode">[<span class="id" type="tactic">intuition</span></span> <span class="inlinecode"><span class="id" type="tactic">eauto</span>]</span>. The tactic <span class="inlinecode"><span class="id" type="var">jauto</span></span> is defined in
    the library <span class="inlinecode"><span class="id" type="var">LibTactics</span></span>, and simply performs some preprocessing
    of the goal before calling <span class="inlinecode"><span class="id" type="tactic">eauto</span></span>. The goal of this chapter is
    to explain the general principles of proof search and to give
    rule of thumbs for guessing which of the four tactics mentioned
    above is best suited for solving a given goal.

<div class="paragraph"> </div>

    Proof search is a compromise between efficiency and
    expressiveness, that is, a tradeoff between how complex goals the
    tactic can solve and how much time the tactic requires for
    terminating. The tactic <span class="inlinecode"><span class="id" type="tactic">auto</span></span> builds proofs only by using the
    basic tactics <span class="inlinecode"><span class="id" type="tactic">reflexivity</span></span>, <span class="inlinecode"><span class="id" type="tactic">assumption</span></span>, and <span class="inlinecode"><span class="id" type="tactic">apply</span></span>. The tactic
    <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> can also exploit <span class="inlinecode"><span class="id" type="tactic">eapply</span></span>. The tactic <span class="inlinecode"><span class="id" type="var">jauto</span></span> extends
    <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> by being able to open conjunctions and existentials that
    occur in the context.  The tactic <span class="inlinecode"><span class="id" type="var">iauto</span></span> is able to deal with
    conjunctions, disjunctions, and negation in a quite clever way;
    however it is not able to open existentials from the context.
    Also, <span class="inlinecode"><span class="id" type="var">iauto</span></span> usually becomes very slow when the goal involves
    several disjunctions.

<div class="paragraph"> </div>

    Note that proof search tactics never perform any rewriting
    step (tactics <span class="inlinecode"><span class="id" type="tactic">rewrite</span></span>, <span class="inlinecode"><span class="id" type="tactic">subst</span></span>), nor any case analysis on an
    arbitrary data structure or property (tactics <span class="inlinecode"><span class="id" type="tactic">destruct</span></span> and
    <span class="inlinecode"><span class="id" type="tactic">inversion</span></span>), nor any proof by induction (tactic <span class="inlinecode"><span class="id" type="tactic">induction</span></span>). So,
    proof search is really intended to automate the final steps from
    the various branches of a proof. It is not able to discover the
    overall structure of a proof. 
</div>

<div class="doc">
<a name="lab547"></a><h2 class="section">Basics</h2>

<div class="paragraph"> </div>

 The tactic <span class="inlinecode"><span class="id" type="tactic">auto</span></span> is able to solve a goal that can be proved
    using a sequence of <span class="inlinecode"><span class="id" type="tactic">intros</span></span>, <span class="inlinecode"><span class="id" type="tactic">apply</span></span>, <span class="inlinecode"><span class="id" type="tactic">assumption</span></span>, and <span class="inlinecode"><span class="id" type="tactic">reflexivity</span></span>.
    Two examples follow. The first one shows the ability for
    <span class="inlinecode"><span class="id" type="tactic">auto</span></span> to call <span class="inlinecode"><span class="id" type="tactic">reflexivity</span></span> at any time. In fact, calling
    <span class="inlinecode"><span class="id" type="tactic">reflexivity</span></span> is always the first thing that <span class="inlinecode"><span class="id" type="tactic">auto</span></span> tries to do. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">solving_by_reflexivity</span> :<br/>
&nbsp;&nbsp;2 + 3 = 5.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">auto</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
The second example illustrates a proof where a sequence of
    two calls to <span class="inlinecode"><span class="id" type="tactic">apply</span></span> are needed. The goal is to prove that
    if <span class="inlinecode"><span class="id" type="var">Q</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> implies <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> for any <span class="inlinecode"><span class="id" type="var">n</span></span> and if <span class="inlinecode"><span class="id" type="var">Q</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> holds for any <span class="inlinecode"><span class="id" type="var">n</span></span>,
    then <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">2</span> holds. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">solving_by_apply</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">P</span> <span class="id" type="var">Q</span> : <span class="id" type="var">nat</span>→<span class="id" type="keyword">Prop</span>),<br/>
&nbsp;&nbsp;(<span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>, <span class="id" type="var">Q</span> <span class="id" type="var">n</span> → <span class="id" type="var">P</span> <span class="id" type="var">n</span>) →<br/>
&nbsp;&nbsp;(<span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>, <span class="id" type="var">Q</span> <span class="id" type="var">n</span>) →<br/>
&nbsp;&nbsp;<span class="id" type="var">P</span> 2.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">auto</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
If we are interested to see which proof <span class="inlinecode"><span class="id" type="tactic">auto</span></span> came up with,
    one possibility is to look at the generated proof-term,
    using the command:

<div class="paragraph"> </div>

       <span class="inlinecode"><span class="id" type="keyword">Print</span></span> <span class="inlinecode"><span class="id" type="var">solving_by_apply</span>.</span>

<div class="paragraph"> </div>

   The proof term is:

<div class="paragraph"> </div>

   <span class="inlinecode"><span class="id" type="keyword">fun</span></span> <span class="inlinecode">(<span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">Q</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" type="var">nat</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="keyword">Prop</span>)</span> <span class="inlinecode">(<span class="id" type="var">H</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span style='font-size:120%;'>&forall;</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" type="var">nat</span>,</span> <span class="inlinecode"><span class="id" type="var">Q</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">n</span>)</span> <span class="inlinecode">(<span class="id" type="var">H<sub>0</sub></span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span style='font-size:120%;'>&forall;</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" type="var">nat</span>,</span> <span class="inlinecode"><span class="id" type="var">Q</span></span> <span class="inlinecode"><span class="id" type="var">n</span>)</span>
     <span class="inlinecode">⇒</span> <span class="inlinecode"><span class="id" type="var">H</span></span> <span class="inlinecode">2</span> <span class="inlinecode">(<span class="id" type="var">H<sub>0</sub></span></span> <span class="inlinecode">2)</span>

<div class="paragraph"> </div>

   This essentially means that <span class="inlinecode"><span class="id" type="tactic">auto</span></span> applied the hypothesis <span class="inlinecode"><span class="id" type="var">H</span></span>
   (the first one), and then applied the hypothesis <span class="inlinecode"><span class="id" type="var">H<sub>0</sub></span></span> (the
   second one).

<div class="paragraph"> </div>


<div class="paragraph"> </div>

 The tactic <span class="inlinecode"><span class="id" type="tactic">auto</span></span> can invoke <span class="inlinecode"><span class="id" type="tactic">apply</span></span> but not <span class="inlinecode"><span class="id" type="tactic">eapply</span></span>. So, <span class="inlinecode"><span class="id" type="tactic">auto</span></span>
    cannot exploit lemmas whose instantiation cannot be directly
    deduced from the proof goal. To exploit such lemmas, one needs to
    invoke the tactic <span class="inlinecode"><span class="id" type="tactic">eauto</span></span>, which is able to call <span class="inlinecode"><span class="id" type="tactic">eapply</span></span>.

<div class="paragraph"> </div>

    In the following example, the first hypothesis asserts that <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span>
    is true when <span class="inlinecode"><span class="id" type="var">Q</span></span> <span class="inlinecode"><span class="id" type="var">m</span></span> is true for some <span class="inlinecode"><span class="id" type="var">m</span></span>, and the goal is to prove
    that <span class="inlinecode"><span class="id" type="var">Q</span></span> <span class="inlinecode">1</span> implies <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">2</span>.  This implication follows directly from
    the hypothesis by instantiating <span class="inlinecode"><span class="id" type="var">m</span></span> as the value <span class="inlinecode">1</span>.  The
    following proof script shows that <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> successfully solves the
    goal, whereas <span class="inlinecode"><span class="id" type="tactic">auto</span></span> is not able to do so. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">solving_by_eapply</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">P</span> <span class="id" type="var">Q</span> : <span class="id" type="var">nat</span>→<span class="id" type="keyword">Prop</span>),<br/>
&nbsp;&nbsp;(<span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span> <span class="id" type="var">m</span>, <span class="id" type="var">Q</span> <span class="id" type="var">m</span> → <span class="id" type="var">P</span> <span class="id" type="var">n</span>) →<br/>
&nbsp;&nbsp;<span class="id" type="var">Q</span> 1 →<br/>
&nbsp;&nbsp;<span class="id" type="var">P</span> 2.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">auto</span>. <span class="id" type="tactic">eauto</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab548"></a><h2 class="section">Conjunctions</h2>

<div class="paragraph"> </div>

 So far, we've seen that <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> is stronger than <span class="inlinecode"><span class="id" type="tactic">auto</span></span> in the
    sense that it can deal with <span class="inlinecode"><span class="id" type="tactic">eapply</span></span>. In the same way, we are going
    to see how <span class="inlinecode"><span class="id" type="var">jauto</span></span> and <span class="inlinecode"><span class="id" type="var">iauto</span></span> are stronger than <span class="inlinecode"><span class="id" type="tactic">auto</span></span> and <span class="inlinecode"><span class="id" type="tactic">eauto</span></span>
    in the sense that they provide better support for conjunctions. 
<div class="paragraph"> </div>

 The tactics <span class="inlinecode"><span class="id" type="tactic">auto</span></span> and <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> can prove a goal of the form
    <span class="inlinecode"><span class="id" type="var">F</span></span> <span class="inlinecode">∧</span> <span class="inlinecode"><span class="id" type="var">F'</span></span>, where <span class="inlinecode"><span class="id" type="var">F</span></span> and <span class="inlinecode"><span class="id" type="var">F'</span></span> are two propositions, as soon as
    both <span class="inlinecode"><span class="id" type="var">F</span></span> and <span class="inlinecode"><span class="id" type="var">F'</span></span> can be proved in the current context.
    An example follows. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">solving_conj_goal</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">P</span> : <span class="id" type="var">nat</span>→<span class="id" type="keyword">Prop</span>) (<span class="id" type="var">F</span> : <span class="id" type="keyword">Prop</span>),<br/>
&nbsp;&nbsp;(<span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>, <span class="id" type="var">P</span> <span class="id" type="var">n</span>) →<br/>
&nbsp;&nbsp;<span class="id" type="var">F</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">F</span> ∧ <span class="id" type="var">P</span> 2.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">auto</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
However, when an assumption is a conjunction, <span class="inlinecode"><span class="id" type="tactic">auto</span></span> and <span class="inlinecode"><span class="id" type="tactic">eauto</span></span>
    are not able to exploit this conjunction. It can be quite
    surprising at first that <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> can prove very complex goals but
    that it fails to prove that <span class="inlinecode"><span class="id" type="var">F</span></span> <span class="inlinecode">∧</span> <span class="inlinecode"><span class="id" type="var">F'</span></span> implies <span class="inlinecode"><span class="id" type="var">F</span></span>. The tactics
    <span class="inlinecode"><span class="id" type="var">iauto</span></span> and <span class="inlinecode"><span class="id" type="var">jauto</span></span> are able to decompose conjunctions from the context.
    Here is an example. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">solving_conj_hyp</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">F</span> <span class="id" type="var">F'</span> : <span class="id" type="keyword">Prop</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">F</span> ∧ <span class="id" type="var">F'</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">F</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">auto</span>. <span class="id" type="tactic">eauto</span>. <span class="id" type="var">jauto</span>. <span class="comment">(*&nbsp;or&nbsp;<span class="inlinecode"><span class="id" type="var">iauto</span></span>&nbsp;*)</span> <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
The tactic <span class="inlinecode"><span class="id" type="var">jauto</span></span> is implemented by first calling a
    pre-processing tactic called <span class="inlinecode"><span class="id" type="var">jauto_set</span></span>, and then calling
    <span class="inlinecode"><span class="id" type="tactic">eauto</span></span>. So, to understand how <span class="inlinecode"><span class="id" type="var">jauto</span></span> works, one can directly
    call the tactic <span class="inlinecode"><span class="id" type="var">jauto_set</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">solving_conj_hyp'</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">F</span> <span class="id" type="var">F'</span> : <span class="id" type="keyword">Prop</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">F</span> ∧ <span class="id" type="var">F'</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">F</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">intros</span>. <span class="id" type="var">jauto_set</span>. <span class="id" type="tactic">eauto</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
Next is a more involved goal that can be solved by <span class="inlinecode"><span class="id" type="var">iauto</span></span> and
    <span class="inlinecode"><span class="id" type="var">jauto</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">solving_conj_more</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">P</span> <span class="id" type="var">Q</span> <span class="id" type="var">R</span> : <span class="id" type="var">nat</span>→<span class="id" type="keyword">Prop</span>) (<span class="id" type="var">F</span> : <span class="id" type="keyword">Prop</span>),<br/>
&nbsp;&nbsp;(<span class="id" type="var">F</span> ∧ (<span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span> <span class="id" type="var">m</span>, (<span class="id" type="var">Q</span> <span class="id" type="var">m</span> ∧ <span class="id" type="var">R</span> <span class="id" type="var">n</span>) → <span class="id" type="var">P</span> <span class="id" type="var">n</span>)) →<br/>
&nbsp;&nbsp;(<span class="id" type="var">F</span> → <span class="id" type="var">R</span> 2) →<br/>
&nbsp;&nbsp;<span class="id" type="var">Q</span> 1 →<br/>
&nbsp;&nbsp;<span class="id" type="var">P</span> 2 ∧ <span class="id" type="var">F</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="var">jauto</span>. <span class="comment">(*&nbsp;or&nbsp;<span class="inlinecode"><span class="id" type="var">iauto</span></span>&nbsp;*)</span> <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
The strategy of <span class="inlinecode"><span class="id" type="var">iauto</span></span> and <span class="inlinecode"><span class="id" type="var">jauto</span></span> is to run a global analysis of
    the top-level conjunctions, and then call <span class="inlinecode"><span class="id" type="tactic">eauto</span></span>.  For this
    reason, those tactics are not good at dealing with conjunctions
    that occur as the conclusion of some universally quantified
    hypothesis. The following example illustrates a general weakness
    of Coq proof search mechanisms. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">solving_conj_hyp_forall</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">P</span> <span class="id" type="var">Q</span> : <span class="id" type="var">nat</span>→<span class="id" type="keyword">Prop</span>),<br/>
&nbsp;&nbsp;(<span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>, <span class="id" type="var">P</span> <span class="id" type="var">n</span> ∧ <span class="id" type="var">Q</span> <span class="id" type="var">n</span>) →<br/>
&nbsp;&nbsp;<span class="id" type="var">P</span> 2.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">auto</span>. <span class="id" type="tactic">eauto</span>. <span class="id" type="var">iauto</span>. <span class="id" type="var">jauto</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;Nothing&nbsp;works,&nbsp;so&nbsp;we&nbsp;have&nbsp;to&nbsp;do&nbsp;some&nbsp;of&nbsp;the&nbsp;work&nbsp;by&nbsp;hand&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span>. <span class="id" type="tactic">destruct</span> (<span class="id" type="var">H</span> 2). <span class="id" type="tactic">auto</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
This situation is slightly disappointing, since automation is
    able to prove the following goal, which is very similar. The
    only difference is that the universal quantification has been
    distributed over the conjunction. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">solved_by_jauto</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">P</span> <span class="id" type="var">Q</span> : <span class="id" type="var">nat</span>→<span class="id" type="keyword">Prop</span>) (<span class="id" type="var">F</span> : <span class="id" type="keyword">Prop</span>),<br/>
&nbsp;&nbsp;(<span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>, <span class="id" type="var">P</span> <span class="id" type="var">n</span>) ∧ (<span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>, <span class="id" type="var">Q</span> <span class="id" type="var">n</span>) →<br/>
&nbsp;&nbsp;<span class="id" type="var">P</span> 2.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="var">jauto</span>. <span class="comment">(*&nbsp;or&nbsp;<span class="inlinecode"><span class="id" type="var">iauto</span></span>&nbsp;*)</span> <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab549"></a><h2 class="section">Disjunctions</h2>

<div class="paragraph"> </div>

 The tactics <span class="inlinecode"><span class="id" type="tactic">auto</span></span> and <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> can handle disjunctions that
    occur in the goal. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">solving_disj_goal</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">F</span> <span class="id" type="var">F'</span> : <span class="id" type="keyword">Prop</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">F</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">F</span> ∨ <span class="id" type="var">F'</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">auto</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
However, only <span class="inlinecode"><span class="id" type="var">iauto</span></span> is able to automate reasoning on the
    disjunctions that appear in the context. For example, <span class="inlinecode"><span class="id" type="var">iauto</span></span> can
    prove that <span class="inlinecode"><span class="id" type="var">F</span></span> <span class="inlinecode">∨</span> <span class="inlinecode"><span class="id" type="var">F'</span></span> entails <span class="inlinecode"><span class="id" type="var">F'</span></span> <span class="inlinecode">∨</span> <span class="inlinecode"><span class="id" type="var">F</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">solving_disj_hyp</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">F</span> <span class="id" type="var">F'</span> : <span class="id" type="keyword">Prop</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">F</span> ∨ <span class="id" type="var">F'</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">F'</span> ∨ <span class="id" type="var">F</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">auto</span>. <span class="id" type="tactic">eauto</span>. <span class="id" type="var">jauto</span>. <span class="id" type="var">iauto</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
More generally, <span class="inlinecode"><span class="id" type="var">iauto</span></span> can deal with complex combinations of
    conjunctions, disjunctions, and negations. Here is an example. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">solving_tauto</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">F<sub>1</sub></span> <span class="id" type="var">F<sub>2</sub></span> <span class="id" type="var">F<sub>3</sub></span> : <span class="id" type="keyword">Prop</span>),<br/>
&nbsp;&nbsp;((¬<span class="id" type="var">F<sub>1</sub></span> ∧ <span class="id" type="var">F<sub>3</sub></span>) ∨ (<span class="id" type="var">F<sub>2</sub></span> ∧ ¬<span class="id" type="var">F<sub>3</sub></span>)) →<br/>
&nbsp;&nbsp;(<span class="id" type="var">F<sub>2</sub></span> → <span class="id" type="var">F<sub>1</sub></span>) →<br/>
&nbsp;&nbsp;(<span class="id" type="var">F<sub>2</sub></span> → <span class="id" type="var">F<sub>3</sub></span>) →<br/>
&nbsp;&nbsp;¬<span class="id" type="var">F<sub>2</sub></span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="var">iauto</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
However, the ability of <span class="inlinecode"><span class="id" type="var">iauto</span></span> to automatically perform a case
    analysis on disjunctions comes with a downside: <span class="inlinecode"><span class="id" type="var">iauto</span></span> may be
    very slow. If the context involves several hypotheses with
    disjunctions, <span class="inlinecode"><span class="id" type="var">iauto</span></span> typically generates an exponential number of
    subgoals on which <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> is called. One major advantage of <span class="inlinecode"><span class="id" type="var">jauto</span></span>
    compared with <span class="inlinecode"><span class="id" type="var">iauto</span></span> is that it never spends time performing this
    kind of case analyses. 
</div>

<div class="doc">
<a name="lab550"></a><h2 class="section">Existentials</h2>

<div class="paragraph"> </div>

 The tactics <span class="inlinecode"><span class="id" type="tactic">eauto</span></span>, <span class="inlinecode"><span class="id" type="var">iauto</span></span>, and <span class="inlinecode"><span class="id" type="var">jauto</span></span> can prove goals whose
    conclusion is an existential. For example, if the goal is <span class="inlinecode"><span style='font-size:120%;'>&exist;</span></span>
    <span class="inlinecode"><span class="id" type="var">x</span>,</span> <span class="inlinecode"><span class="id" type="var">f</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span>, the tactic <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> introduces an existential variable,
    say <span class="inlinecode">?25</span>, in place of <span class="inlinecode"><span class="id" type="var">x</span></span>. The remaining goal is <span class="inlinecode"><span class="id" type="var">f</span></span> <span class="inlinecode">?25</span>, and
    <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> tries to solve this goal, allowing itself to instantiate
    <span class="inlinecode">?25</span> with any appropriate value. For example, if an assumption
    <span class="inlinecode"><span class="id" type="var">f</span></span> <span class="inlinecode">2</span> is available, then the variable <span class="inlinecode">?25</span> gets instantiated with
    <span class="inlinecode">2</span> and the goal is solved, as shown below. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">solving_exists_goal</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">f</span> : <span class="id" type="var">nat</span>→<span class="id" type="keyword">Prop</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">f</span> 2 →<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">x</span>, <span class="id" type="var">f</span> <span class="id" type="var">x</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">auto</span>. <span class="comment">(*&nbsp;observe&nbsp;that&nbsp;<span class="inlinecode"><span class="id" type="tactic">auto</span></span>&nbsp;does&nbsp;not&nbsp;deal&nbsp;with&nbsp;existentials,&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="tactic">eauto</span>. <span class="comment">(*&nbsp;whereas&nbsp;<span class="inlinecode"><span class="id" type="tactic">eauto</span></span>,&nbsp;<span class="inlinecode"><span class="id" type="var">iauto</span></span>&nbsp;and&nbsp;<span class="inlinecode"><span class="id" type="var">jauto</span></span>&nbsp;solve&nbsp;the&nbsp;goal&nbsp;*)</span><br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
A major strength of <span class="inlinecode"><span class="id" type="var">jauto</span></span> over the other proof search tactics is
    that it is able to exploit the existentially-quantified
    hypotheses, i.e., those of the form <span class="inlinecode"><span style='font-size:120%;'>&exist;</span></span> <span class="inlinecode"><span class="id" type="var">x</span>,</span> <span class="inlinecode"><span class="id" type="var">P</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">solving_exists_hyp</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">f</span> <span class="id" type="var">g</span> : <span class="id" type="var">nat</span>→<span class="id" type="keyword">Prop</span>),<br/>
&nbsp;&nbsp;(<span style='font-size:120%;'>&forall;</span><span class="id" type="var">x</span>, <span class="id" type="var">f</span> <span class="id" type="var">x</span> → <span class="id" type="var">g</span> <span class="id" type="var">x</span>) →<br/>
&nbsp;&nbsp;(<span style='font-size:120%;'>&exist;</span><span class="id" type="var">a</span>, <span class="id" type="var">f</span> <span class="id" type="var">a</span>) →<br/>
&nbsp;&nbsp;(<span style='font-size:120%;'>&exist;</span><span class="id" type="var">a</span>, <span class="id" type="var">g</span> <span class="id" type="var">a</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">auto</span>. <span class="id" type="tactic">eauto</span>. <span class="id" type="var">iauto</span>. <span class="comment">(*&nbsp;All&nbsp;of&nbsp;these&nbsp;tactics&nbsp;fail,&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="var">jauto</span>. <span class="comment">(*&nbsp;whereas&nbsp;<span class="inlinecode"><span class="id" type="var">jauto</span></span>&nbsp;succeeds.&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;For&nbsp;the&nbsp;details,&nbsp;run&nbsp;<span class="inlinecode"><span class="id" type="tactic">intros</span>.</span> <span class="inlinecode"><span class="id" type="var">jauto_set</span>.</span> <span class="inlinecode"><span class="id" type="tactic">eauto</span></span>&nbsp;*)</span><br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab551"></a><h2 class="section">Negation</h2>

<div class="paragraph"> </div>

 The tactics <span class="inlinecode"><span class="id" type="tactic">auto</span></span> and <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> suffer from some limitations with
    respect to the manipulation of negations, mostly related to the
    fact that negation, written <span class="inlinecode">¬</span> <span class="inlinecode"><span class="id" type="var">P</span></span>, is defined as <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">False</span></span> but
    that the unfolding of this definition is not performed
    automatically. Consider the following example. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">negation_study_1</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">P</span> : <span class="id" type="var">nat</span>→<span class="id" type="keyword">Prop</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">P</span> 0 →<br/>
&nbsp;&nbsp;(<span style='font-size:120%;'>&forall;</span><span class="id" type="var">x</span>, ¬<span class="id" type="var">P</span> <span class="id" type="var">x</span>) →<br/>
&nbsp;&nbsp;<span class="id" type="var">False</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">P</span> <span class="id" type="var">H<sub>0</sub></span> <span class="id" type="var">HX</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">eauto</span>. <span class="comment">(*&nbsp;It&nbsp;fails&nbsp;to&nbsp;see&nbsp;that&nbsp;<span class="inlinecode"><span class="id" type="var">HX</span></span>&nbsp;applies&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">not</span> <span class="id" type="keyword">in</span> *. <span class="id" type="tactic">eauto</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
For this reason, the tactics <span class="inlinecode"><span class="id" type="var">iauto</span></span> and <span class="inlinecode"><span class="id" type="var">jauto</span></span> systematically
    invoke <span class="inlinecode"><span class="id" type="tactic">unfold</span></span> <span class="inlinecode"><span class="id" type="var">not</span></span> <span class="inlinecode"><span class="id" type="keyword">in</span></span> <span class="inlinecode">*</span> as part of their pre-processing. So,
    they are able to solve the previous goal right away. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">negation_study_2</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">P</span> : <span class="id" type="var">nat</span>→<span class="id" type="keyword">Prop</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">P</span> 0 →<br/>
&nbsp;&nbsp;(<span style='font-size:120%;'>&forall;</span><span class="id" type="var">x</span>, ¬<span class="id" type="var">P</span> <span class="id" type="var">x</span>) →<br/>
&nbsp;&nbsp;<span class="id" type="var">False</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="var">jauto</span>. <span class="comment">(*&nbsp;or&nbsp;<span class="inlinecode"><span class="id" type="var">iauto</span></span>&nbsp;*)</span> <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
We will come back later on to the behavior of proof search with
    respect to the unfolding of definitions. 
</div>

<div class="doc">
<a name="lab552"></a><h2 class="section">Equalities</h2>

<div class="paragraph"> </div>

 Coq's proof-search feature is not good at exploiting equalities.
    It can do very basic operations, like exploiting reflexivity
    and symmetry, but that's about it. Here is a simple example
    that <span class="inlinecode"><span class="id" type="tactic">auto</span></span> can solve, by first calling <span class="inlinecode"><span class="id" type="tactic">symmetry</span></span> and then
    applying the hypothesis. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">equality_by_auto</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">f</span> <span class="id" type="var">g</span> : <span class="id" type="var">nat</span>→<span class="id" type="keyword">Prop</span>),<br/>
&nbsp;&nbsp;(<span style='font-size:120%;'>&forall;</span><span class="id" type="var">x</span>, <span class="id" type="var">f</span> <span class="id" type="var">x</span> = <span class="id" type="var">g</span> <span class="id" type="var">x</span>) →<br/>
&nbsp;&nbsp;<span class="id" type="var">g</span> 2 = <span class="id" type="var">f</span> 2.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">auto</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
To automate more advanced reasoning on equalities, one should
    rather try to use the tactic <span class="inlinecode"><span class="id" type="tactic">congruence</span></span>, which is presented at
    the end of this chapter in the "Decision Procedures" section. 
</div>

<div class="doc">
<a name="lab553"></a><h1 class="section">How Proof Search Works</h1>

</div>
<div class="code code-space">

<br/>
</div>

<div class="doc">
<a name="lab554"></a><h2 class="section">Search Depth</h2>

<div class="paragraph"> </div>

 The tactic <span class="inlinecode"><span class="id" type="tactic">auto</span></span> works as follows.  It first tries to call
    <span class="inlinecode"><span class="id" type="tactic">reflexivity</span></span> and <span class="inlinecode"><span class="id" type="tactic">assumption</span></span>. If one of these calls solves the
    goal, the job is done. Otherwise <span class="inlinecode"><span class="id" type="tactic">auto</span></span> tries to apply the most
    recently introduced assumption that can be applied to the goal
    without producing and error. This application produces
    subgoals. There are two possible cases. If the sugboals produced
    can be solved by a recursive call to <span class="inlinecode"><span class="id" type="tactic">auto</span></span>, then the job is done.
    Otherwise, if this application produces at least one subgoal that
    <span class="inlinecode"><span class="id" type="tactic">auto</span></span> cannot solve, then <span class="inlinecode"><span class="id" type="tactic">auto</span></span> starts over by trying to apply
    the second most recently introduced assumption. It continues in a
    similar fashion until it finds a proof or until no assumption
    remains to be tried.

<div class="paragraph"> </div>

    It is very important to have a clear idea of the backtracking
    process involved in the execution of the <span class="inlinecode"><span class="id" type="tactic">auto</span></span> tactic; otherwise
    its behavior can be quite puzzling. For example, <span class="inlinecode"><span class="id" type="tactic">auto</span></span> is not
    able to solve the following triviality. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">search_depth_0</span> :<br/>
&nbsp;&nbsp;<span class="id" type="var">True</span> ∧ <span class="id" type="var">True</span> ∧ <span class="id" type="var">True</span> ∧ <span class="id" type="var">True</span> ∧ <span class="id" type="var">True</span> ∧ <span class="id" type="var">True</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">auto</span>.<br/>
<span class="id" type="keyword">Abort</span>.<br/>
</div>

<div class="doc">
The reason <span class="inlinecode"><span class="id" type="tactic">auto</span></span> fails to solve the goal is because there are
    too many conjunctions. If there had been only five of them, <span class="inlinecode"><span class="id" type="tactic">auto</span></span>
    would have successfully solved the proof, but six is too many.
    The tactic <span class="inlinecode"><span class="id" type="tactic">auto</span></span> limits the number of lemmas and hypotheses
    that can be applied in a proof, so as to ensure that the proof
    search eventually terminates. By default, the maximal number
    of steps is five. One can specify a different bound, writing
    for example <span class="inlinecode"><span class="id" type="tactic">auto</span></span> <span class="inlinecode">6</span> to search for a proof involving at most
    six steps. For example, <span class="inlinecode"><span class="id" type="tactic">auto</span></span> <span class="inlinecode">6</span> would solve the previous lemma.
    (Similarly, one can invoke <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> <span class="inlinecode">6</span> or <span class="inlinecode"><span class="id" type="tactic">intuition</span></span> <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> <span class="inlinecode">6</span>.)
    The argument <span class="inlinecode"><span class="id" type="var">n</span></span> of <span class="inlinecode"><span class="id" type="tactic">auto</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> is called the "search depth."
    The tactic <span class="inlinecode"><span class="id" type="tactic">auto</span></span> is simply defined as a shorthand for <span class="inlinecode"><span class="id" type="tactic">auto</span></span> <span class="inlinecode">5</span>.

<div class="paragraph"> </div>

    The behavior of <span class="inlinecode"><span class="id" type="tactic">auto</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> can be summarized as follows. It first
    tries to solve the goal using <span class="inlinecode"><span class="id" type="tactic">reflexivity</span></span> and <span class="inlinecode"><span class="id" type="tactic">assumption</span></span>. If
    this fails, it tries to apply a hypothesis (or a lemma that has
    been registered in the hint database), and this application
    produces a number of sugoals. The tactic <span class="inlinecode"><span class="id" type="tactic">auto</span></span> <span class="inlinecode">(<span class="id" type="var">n</span>-1)</span> is then
    called on each of those subgoals. If all the subgoals are solved,
    the job is completed, otherwise <span class="inlinecode"><span class="id" type="tactic">auto</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> tries to apply a
    different hypothesis.

<div class="paragraph"> </div>

    During the process, <span class="inlinecode"><span class="id" type="tactic">auto</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> calls <span class="inlinecode"><span class="id" type="tactic">auto</span></span> <span class="inlinecode">(<span class="id" type="var">n</span>-1)</span>, which in turn
    might call <span class="inlinecode"><span class="id" type="tactic">auto</span></span> <span class="inlinecode">(<span class="id" type="var">n</span>-2)</span>, and so on. The tactic <span class="inlinecode"><span class="id" type="tactic">auto</span></span> <span class="inlinecode">0</span> only
    tries <span class="inlinecode"><span class="id" type="tactic">reflexivity</span></span> and <span class="inlinecode"><span class="id" type="tactic">assumption</span></span>, and does not try to apply
    any lemma. Overall, this means that when the maximal number of
    steps allowed has been exceeded, the <span class="inlinecode"><span class="id" type="tactic">auto</span></span> tactic stops searching
    and backtracks to try and investigate other paths. 
<div class="paragraph"> </div>

 The following lemma admits a unique proof that involves exactly
    three steps. So, <span class="inlinecode"><span class="id" type="tactic">auto</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> proves this goal iff <span class="inlinecode"><span class="id" type="var">n</span></span> is greater than
    three. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">search_depth_1</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">P</span> : <span class="id" type="var">nat</span>→<span class="id" type="keyword">Prop</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">P</span> 0 →<br/>
&nbsp;&nbsp;(<span class="id" type="var">P</span> 0 → <span class="id" type="var">P</span> 1) →<br/>
&nbsp;&nbsp;(<span class="id" type="var">P</span> 1 → <span class="id" type="var">P</span> 2) →<br/>
&nbsp;&nbsp;(<span class="id" type="var">P</span> 2).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">auto</span> 0. <span class="comment">(*&nbsp;does&nbsp;not&nbsp;find&nbsp;the&nbsp;proof&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="tactic">auto</span> 1. <span class="comment">(*&nbsp;does&nbsp;not&nbsp;find&nbsp;the&nbsp;proof&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="tactic">auto</span> 2. <span class="comment">(*&nbsp;does&nbsp;not&nbsp;find&nbsp;the&nbsp;proof&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="tactic">auto</span> 3. <span class="comment">(*&nbsp;finds&nbsp;the&nbsp;proof&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;more&nbsp;generally,&nbsp;<span class="inlinecode"><span class="id" type="tactic">auto</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span>&nbsp;solves&nbsp;the&nbsp;goal&nbsp;if&nbsp;<span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">≥</span> <span class="inlinecode">3</span>&nbsp;*)</span><br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
We can generalize the example by introducing an assumption
    asserting that <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">k</span></span> is derivable from <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">(<span class="id" type="var">k</span>-1)</span> for all <span class="inlinecode"><span class="id" type="var">k</span></span>,
    and keep the assumption <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">0</span>. The tactic <span class="inlinecode"><span class="id" type="tactic">auto</span></span>, which is the
    same as <span class="inlinecode"><span class="id" type="tactic">auto</span></span> <span class="inlinecode">5</span>, is able to derive <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">k</span></span> for all values of <span class="inlinecode"><span class="id" type="var">k</span></span>
    less than 5. For example, it can prove <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">4</span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">search_depth_3</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">P</span> : <span class="id" type="var">nat</span>→<span class="id" type="keyword">Prop</span>),<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;Hypothesis&nbsp;H<sub>1</sub>:&nbsp;*)</span> (<span class="id" type="var">P</span> 0) →<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;Hypothesis&nbsp;H<sub>2</sub>:&nbsp;*)</span> (<span style='font-size:120%;'>&forall;</span><span class="id" type="var">k</span>, <span class="id" type="var">P</span> (<span class="id" type="var">k</span>-1) → <span class="id" type="var">P</span> <span class="id" type="var">k</span>) →<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;Goal:&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;*)</span> (<span class="id" type="var">P</span> 4).<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">auto</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
However, to prove <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">5</span>, one needs to call at least <span class="inlinecode"><span class="id" type="tactic">auto</span></span> <span class="inlinecode">6</span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">search_depth_4</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">P</span> : <span class="id" type="var">nat</span>→<span class="id" type="keyword">Prop</span>),<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;Hypothesis&nbsp;H<sub>1</sub>:&nbsp;*)</span> (<span class="id" type="var">P</span> 0) →<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;Hypothesis&nbsp;H<sub>2</sub>:&nbsp;*)</span> (<span style='font-size:120%;'>&forall;</span><span class="id" type="var">k</span>, <span class="id" type="var">P</span> (<span class="id" type="var">k</span>-1) → <span class="id" type="var">P</span> <span class="id" type="var">k</span>) →<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;Goal:&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;*)</span> (<span class="id" type="var">P</span> 5).<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">auto</span>. <span class="id" type="tactic">auto</span> 6. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
Because <span class="inlinecode"><span class="id" type="tactic">auto</span></span> looks for proofs at a limited depth, there are
    cases where <span class="inlinecode"><span class="id" type="tactic">auto</span></span> can prove a goal <span class="inlinecode"><span class="id" type="var">F</span></span> and can prove a goal
    <span class="inlinecode"><span class="id" type="var">F'</span></span> but cannot prove <span class="inlinecode"><span class="id" type="var">F</span></span> <span class="inlinecode">∧</span> <span class="inlinecode"><span class="id" type="var">F'</span></span>. In the following example,
    <span class="inlinecode"><span class="id" type="tactic">auto</span></span> can prove <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">4</span> but it is not able to prove <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">4</span> <span class="inlinecode">∧</span> <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">4</span>,
    because the splitting of the conjunction consumes one proof step.
    To prove the conjunction, one needs to increase the search depth,
    using at least <span class="inlinecode"><span class="id" type="tactic">auto</span></span> <span class="inlinecode">6</span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">search_depth_5</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">P</span> : <span class="id" type="var">nat</span>→<span class="id" type="keyword">Prop</span>),<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;Hypothesis&nbsp;H<sub>1</sub>:&nbsp;*)</span> (<span class="id" type="var">P</span> 0) →<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;Hypothesis&nbsp;H<sub>2</sub>:&nbsp;*)</span> (<span style='font-size:120%;'>&forall;</span><span class="id" type="var">k</span>, <span class="id" type="var">P</span> (<span class="id" type="var">k</span>-1) → <span class="id" type="var">P</span> <span class="id" type="var">k</span>) →<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;Goal:&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;*)</span> (<span class="id" type="var">P</span> 4 ∧ <span class="id" type="var">P</span> 4).<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">auto</span>. <span class="id" type="tactic">auto</span> 6. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab555"></a><h2 class="section">Backtracking</h2>

<div class="paragraph"> </div>

 In the previous section, we have considered proofs where
    at each step there was a unique assumption that <span class="inlinecode"><span class="id" type="tactic">auto</span></span>
    could apply. In general, <span class="inlinecode"><span class="id" type="tactic">auto</span></span> can have several choices
    at every step. The strategy of <span class="inlinecode"><span class="id" type="tactic">auto</span></span> consists of trying all
    of the possibilities (using a depth-first search exploration).

<div class="paragraph"> </div>

    To illustrate how automation works, we are going to extend the
    previous example with an additional assumption asserting that
    <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">k</span></span> is also derivable from <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">(<span class="id" type="var">k</span>+1)</span>. Adding this hypothesis
    offers a new possibility that <span class="inlinecode"><span class="id" type="tactic">auto</span></span> could consider at every step.

<div class="paragraph"> </div>

    There exists a special command that one can use for tracing
    all the steps that proof-search considers. To view such a
    trace, one should write <span class="inlinecode"><span class="id" type="var">debug</span></span> <span class="inlinecode"><span class="id" type="tactic">eauto</span></span>. (For some reason, the
    command <span class="inlinecode"><span class="id" type="var">debug</span></span> <span class="inlinecode"><span class="id" type="tactic">auto</span></span> does not exist, so we have to use the
    command <span class="inlinecode"><span class="id" type="var">debug</span></span> <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> instead.) 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">working_of_auto_1</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">P</span> : <span class="id" type="var">nat</span>→<span class="id" type="keyword">Prop</span>),<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;Hypothesis&nbsp;H<sub>1</sub>:&nbsp;*)</span> (<span class="id" type="var">P</span> 0) →<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;Hypothesis&nbsp;H<sub>2</sub>:&nbsp;*)</span> (<span style='font-size:120%;'>&forall;</span><span class="id" type="var">k</span>, <span class="id" type="var">P</span> (<span class="id" type="var">k</span>-1) → <span class="id" type="var">P</span> <span class="id" type="var">k</span>) →<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;Hypothesis&nbsp;H<sub>3</sub>:&nbsp;*)</span> (<span style='font-size:120%;'>&forall;</span><span class="id" type="var">k</span>, <span class="id" type="var">P</span> (<span class="id" type="var">k</span>+1) → <span class="id" type="var">P</span> <span class="id" type="var">k</span>) →<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;Goal:&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;*)</span> (<span class="id" type="var">P</span> 2).<br/>
<span class="comment">(*&nbsp;Uncomment&nbsp;"debug"&nbsp;in&nbsp;the&nbsp;following&nbsp;line&nbsp;to&nbsp;see&nbsp;the&nbsp;debug&nbsp;trace:&nbsp;*)</span><br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">P</span> <span class="id" type="var">H<sub>1</sub></span> <span class="id" type="var">H<sub>2</sub></span> <span class="id" type="var">H<sub>3</sub></span>. <span class="comment">(*&nbsp;debug&nbsp;*)</span> <span class="id" type="tactic">eauto</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
The output message produced by <span class="inlinecode"><span class="id" type="var">debug</span></span> <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> is as follows.
<pre>
  1 depth=5
  1.1 depth=4 simple apply H<sub>2</sub>
  1.1.1 depth=3 simple apply H<sub>2</sub>
  1.1.1.1 depth=3 exact H<sub>1</sub>
</pre>
    The depth indicates the value of <span class="inlinecode"><span class="id" type="var">n</span></span> with which <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> is
    called. The tactics shown in the message indicate that the first
    thing that <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> has tried to do is to apply <span class="inlinecode"><span class="id" type="var">H<sub>2</sub></span></span>. The effect of
    applying <span class="inlinecode"><span class="id" type="var">H<sub>2</sub></span></span> is to replace the goal <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">2</span> with the goal <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">1</span>.
    Then, again, <span class="inlinecode"><span class="id" type="var">H<sub>2</sub></span></span> has been applied, changing the goal <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">1</span> into
    <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">0</span>. At that point, the goal was exactly the hypothesis <span class="inlinecode"><span class="id" type="var">H<sub>1</sub></span></span>.

<div class="paragraph"> </div>

    It seems that <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> was quite lucky there, as it never even
    tried to use the hypothesis <span class="inlinecode"><span class="id" type="var">H<sub>3</sub></span></span> at any time. The reason is that
    <span class="inlinecode"><span class="id" type="tactic">auto</span></span> always tried to use the <span class="inlinecode"><span class="id" type="var">H<sub>2</sub></span></span> first. So, let's permute
    the hypotheses <span class="inlinecode"><span class="id" type="var">H<sub>2</sub></span></span> and <span class="inlinecode"><span class="id" type="var">H<sub>3</sub></span></span> and see what happens. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">working_of_auto_2</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">P</span> : <span class="id" type="var">nat</span>→<span class="id" type="keyword">Prop</span>),<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;Hypothesis&nbsp;H<sub>1</sub>:&nbsp;*)</span> (<span class="id" type="var">P</span> 0) →<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;Hypothesis&nbsp;H<sub>3</sub>:&nbsp;*)</span> (<span style='font-size:120%;'>&forall;</span><span class="id" type="var">k</span>, <span class="id" type="var">P</span> (<span class="id" type="var">k</span>+1) → <span class="id" type="var">P</span> <span class="id" type="var">k</span>) →<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;Hypothesis&nbsp;H<sub>2</sub>:&nbsp;*)</span> (<span style='font-size:120%;'>&forall;</span><span class="id" type="var">k</span>, <span class="id" type="var">P</span> (<span class="id" type="var">k</span>-1) → <span class="id" type="var">P</span> <span class="id" type="var">k</span>) →<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;Goal:&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;*)</span> (<span class="id" type="var">P</span> 2).<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">P</span> <span class="id" type="var">H<sub>1</sub></span> <span class="id" type="var">H<sub>3</sub></span> <span class="id" type="var">H<sub>2</sub></span>. <span class="comment">(*&nbsp;debug&nbsp;*)</span> <span class="id" type="tactic">eauto</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
This time, the output message suggests that the proof search
    investigates many possibilities. If we print the proof term:

<div class="paragraph"> </div>

      <span class="inlinecode"><span class="id" type="keyword">Print</span></span> <span class="inlinecode"><span class="id" type="var">working_of_auto_2</span>.</span>

<div class="paragraph"> </div>

    we observe that the proof term refers to <span class="inlinecode"><span class="id" type="var">H<sub>3</sub></span></span>. Thus the proof
    is not the simplest one, since only <span class="inlinecode"><span class="id" type="var">H<sub>2</sub></span></span> and <span class="inlinecode"><span class="id" type="var">H<sub>1</sub></span></span> are needed.

<div class="paragraph"> </div>

    In turns out that the proof goes through the proof obligation <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">3</span>,
    even though it is not required to do so. The following tree drawing
    describes all the goals that <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> has been going through.
<pre>
    |5||4||3||2||1||0| -- below, tabulation indicates the depth

    [P 2]
    <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> [P 3]
       <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> [P 4]
          <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> [P 5]
             <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> [P 6]
                <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> [P 7]
                <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> [P 5]
             <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> [P 4]
                <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> [P 5]
                <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> [P 3]
          <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> [P 3]
             <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> [P 4]
                <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> [P 5]
                <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> [P 3]
             <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> [P 2]
                <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> [P 3]
                <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> [P 1]
       <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> [P 2]
          <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> [P 3]
             <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> [P 4]
                <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> [P 5]
                <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> [P 3]
             <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> [P 2]
                <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> [P 3]
                <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> [P 1]
          <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> [P 1]
             <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> [P 2]
                <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> [P 3]
                <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> [P 1]
             <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> [P 0]
                <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> !! Done !!
</pre>
    The first few lines read as follows. To prove <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">2</span>, <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> <span class="inlinecode">5</span>
    has first tried to apply <span class="inlinecode"><span class="id" type="var">H<sub>3</sub></span></span>, producing the subgoal <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">3</span>.
    To solve it, <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> <span class="inlinecode">4</span> has tried again to apply <span class="inlinecode"><span class="id" type="var">H<sub>3</sub></span></span>, producing
    the goal <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">4</span>. Similarly, the search goes through <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">5</span>, <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">6</span>
    and <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">7</span>. When reaching <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">7</span>, the tactic <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> <span class="inlinecode">0</span> is called
    but as it is not allowed to try and apply any lemma, it fails.
    So, we come back to the goal <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">6</span>, and try this time to apply
    hypothesis <span class="inlinecode"><span class="id" type="var">H<sub>2</sub></span></span>, producing the subgoal <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">5</span>. Here again,
    <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> <span class="inlinecode">0</span> fails to solve this goal.

<div class="paragraph"> </div>

    The process goes on and on, until backtracking to <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">3</span> and trying
    to apply <span class="inlinecode"><span class="id" type="var">H<sub>3</sub></span></span> three times in a row, going through <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">2</span> and <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">1</span>
    and <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">0</span>. This search tree explains why <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> came up with a
    proof term starting with an application of <span class="inlinecode"><span class="id" type="var">H<sub>3</sub></span></span>. 
</div>

<div class="doc">
<a name="lab556"></a><h2 class="section">Adding Hints</h2>

<div class="paragraph"> </div>

 By default, <span class="inlinecode"><span class="id" type="tactic">auto</span></span> (and <span class="inlinecode"><span class="id" type="tactic">eauto</span></span>) only tries to apply the
    hypotheses that appear in the proof context. There are two
    possibilities for telling <span class="inlinecode"><span class="id" type="tactic">auto</span></span> to exploit a lemma that have
    been proved previously: either adding the lemma as an assumption
    just before calling <span class="inlinecode"><span class="id" type="tactic">auto</span></span>, or adding the lemma as a hint, so
    that it can be used by every calls to <span class="inlinecode"><span class="id" type="tactic">auto</span></span>.

<div class="paragraph"> </div>

    The first possibility is useful to have <span class="inlinecode"><span class="id" type="tactic">auto</span></span> exploit a lemma
    that only serves at this particular point. To add the lemma as
    hypothesis, one can type <span class="inlinecode"><span class="id" type="tactic">generalize</span></span> <span class="inlinecode"><span class="id" type="var">mylemma</span>;</span> <span class="inlinecode"><span class="id" type="tactic">intros</span></span>, or simply
    <span class="inlinecode"><span class="id" type="var">lets</span>:</span> <span class="inlinecode"><span class="id" type="var">mylemma</span></span> (the latter requires <span class="inlinecode"><span class="id" type="var">LibTactics.v</span></span>).

<div class="paragraph"> </div>

    The second possibility is useful for lemmas that need to be
    exploited several times. The syntax for adding a lemma as a hint
    is <span class="inlinecode"><span class="id" type="keyword">Hint</span></span> <span class="inlinecode"><span class="id" type="keyword">Resolve</span></span> <span class="inlinecode"><span class="id" type="var">mylemma</span></span>. For example: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">nat_le_refl</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">x</span>:<span class="id" type="var">nat</span>), <span class="id" type="var">x</span> ≤ <span class="id" type="var">x</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">le_n</span>. <span class="id" type="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Hint</span> <span class="id" type="keyword">Resolve</span> <span class="id" type="var">nat_le_refl</span>.<br/>
</div>

<div class="doc">
A convenient shorthand for adding all the constructors of an
    inductive datatype as hints is the command <span class="inlinecode"><span class="id" type="keyword">Hint</span></span> <span class="inlinecode"><span class="id" type="var">Constructors</span></span>
    <span class="inlinecode"><span class="id" type="var">mydatatype</span></span>.

<div class="paragraph"> </div>

    Warning: some lemmas, such as transitivity results, should
    not be added as hints as they would very badly affect the
    performance of proof search. The description of this problem
    and the presentation of a general work-around for transitivity
    lemmas appear further on. 
</div>

<div class="doc">
<a name="lab557"></a><h2 class="section">Integration of Automation in Tactics</h2>

<div class="paragraph"> </div>

 The library "LibTactics" introduces a convenient feature for
    invoking automation after calling a tactic. In short, it suffices
    to add the symbol star (<span class="inlinecode">*</span>) to the name of a tactic. For example,
    <span class="inlinecode"><span class="id" type="tactic">apply</span>*</span> <span class="inlinecode"><span class="id" type="var">H</span></span> is equivalent to <span class="inlinecode"><span class="id" type="tactic">apply</span></span> <span class="inlinecode"><span class="id" type="var">H</span>;</span> <span class="inlinecode"><span class="id" type="var">auto_star</span></span>, where <span class="inlinecode"><span class="id" type="var">auto_star</span></span>
    is a tactic that can be defined as needed.

<div class="paragraph"> </div>

    The definition of <span class="inlinecode"><span class="id" type="var">auto_star</span></span>, which determines the meaning of the
    star symbol, can be modified whenever needed. Simply write:

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">Ltac</span>&nbsp;<span class="id" type="var">auto_star</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">a_new_definition</span>.
<div class="paragraph"> </div>

</div>
    Observe the use of <span class="inlinecode"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span></span> instead of <span class="inlinecode">:=</span>, which indicates that the
    tactic is being rebound to a new definition. So, the default
    definition is as follows. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Ltac</span> <span class="id" type="var">auto_star</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="tactic">try</span> <span class="id" type="var">solve</span> [ <span class="id" type="var">jauto</span> ].<br/>
</div>

<div class="doc">
Nearly all standard Coq tactics and all the tactics from
    "LibTactics" can be called with a star symbol. For example, one
    can invoke <span class="inlinecode"><span class="id" type="tactic">subst</span>*</span>, <span class="inlinecode"><span class="id" type="tactic">destruct</span>*</span> <span class="inlinecode"><span class="id" type="var">H</span></span>, <span class="inlinecode"><span class="id" type="var">inverts</span>*</span> <span class="inlinecode"><span class="id" type="var">H</span></span>, <span class="inlinecode"><span class="id" type="var">lets</span>*</span> <span class="inlinecode"><span class="id" type="var">I</span>:</span> <span class="inlinecode"><span class="id" type="var">H</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span>,
    <span class="inlinecode"><span class="id" type="var">specializes</span>*</span> <span class="inlinecode"><span class="id" type="var">H</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span>, and so on... There are two notable exceptions.
    The tactic <span class="inlinecode"><span class="id" type="tactic">auto</span>*</span> is just another name for the tactic
    <span class="inlinecode"><span class="id" type="var">auto_star</span></span>.  And the tactic <span class="inlinecode"><span class="id" type="tactic">apply</span>*</span> <span class="inlinecode"><span class="id" type="var">H</span></span> calls <span class="inlinecode"><span class="id" type="tactic">eapply</span></span> <span class="inlinecode"><span class="id" type="var">H</span></span> (or the
    more powerful <span class="inlinecode"><span class="id" type="var">applys</span></span> <span class="inlinecode"><span class="id" type="var">H</span></span> if needed), and then calls <span class="inlinecode"><span class="id" type="var">auto_star</span></span>.
    Note that there is no <span class="inlinecode"><span class="id" type="tactic">eapply</span>*</span> <span class="inlinecode"><span class="id" type="var">H</span></span> tactic, use <span class="inlinecode"><span class="id" type="tactic">apply</span>*</span> <span class="inlinecode"><span class="id" type="var">H</span></span>
    instead. 
<div class="paragraph"> </div>

 In large developments, it can be convenient to use two degrees of
    automation. Typically, one would use a fast tactic, like <span class="inlinecode"><span class="id" type="tactic">auto</span></span>,
    and a slower but more powerful tactic, like <span class="inlinecode"><span class="id" type="var">jauto</span></span>. To allow for
    a smooth coexistence of the two form of automation, <span class="inlinecode"><span class="id" type="var">LibTactics.v</span></span>
    also defines a "tilde" version of tactics, like <span class="inlinecode"><span class="id" type="tactic">apply</span>¬</span> <span class="inlinecode"><span class="id" type="var">H</span></span>,
    <span class="inlinecode"><span class="id" type="tactic">destruct</span>¬</span> <span class="inlinecode"><span class="id" type="var">H</span></span>, <span class="inlinecode"><span class="id" type="tactic">subst</span>¬</span>, <span class="inlinecode"><span class="id" type="tactic">auto</span>¬</span> and so on. The meaning of the
    tilde symbol is described by the <span class="inlinecode"><span class="id" type="var">auto_tilde</span></span> tactic, whose
    default implementation is <span class="inlinecode"><span class="id" type="tactic">auto</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Ltac</span> <span class="id" type="var">auto_tilde</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="tactic">auto</span>.<br/>
</div>

<div class="doc">
In the examples that follow, only <span class="inlinecode"><span class="id" type="var">auto_star</span></span> is needed. 
<div class="paragraph"> </div>

 An alternative, possibly more efficient version of auto_star is the
    following":

<div class="paragraph"> </div>

    Ltac auto_star <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> try solve <span class="inlinecode"></span> <span class="inlinecode"><span class="id" type="var">eassumption</span></span> <span class="inlinecode">|</span> <span class="inlinecode"><span class="id" type="tactic">auto</span></span> <span class="inlinecode">|</span> <span class="inlinecode"><span class="id" type="var">jauto</span></span> <span class="inlinecode"></span>.

<div class="paragraph"> </div>

    With the above definition, <span class="inlinecode"><span class="id" type="var">auto_star</span></span> first tries to solve the
    goal using the assumptions; if it fails, it tries using <span class="inlinecode"><span class="id" type="tactic">auto</span></span>,
    and if this still fails, then it calls <span class="inlinecode"><span class="id" type="var">jauto</span></span>. Even though
    <span class="inlinecode"><span class="id" type="var">jauto</span></span> is strictly stronger than <span class="inlinecode"><span class="id" type="var">eassumption</span></span> and <span class="inlinecode"><span class="id" type="tactic">auto</span></span>, it
    makes sense to call these tactics first, because, when the
    succeed, they save a lot of time, and when they fail to prove
    the goal, they fail very quickly.".

<div class="paragraph"> </div>


</div>

<div class="doc">
<a name="lab558"></a><h1 class="section">Example Proofs using Automation</h1>

<div class="paragraph"> </div>

 Let's see how to use proof search in practice on the main theorems
    of the "Software Foundations" course, proving in particular
    results such as determinism, preservation and progress. 
</div>

<div class="doc">
<a name="lab559"></a><h2 class="section">Determinism</h2>

</div>
<div class="code code-space">

<br/>
<span class="id" type="keyword">Module</span> <span class="id" type="var">DeterministicImp</span>.<br/>
&nbsp;&nbsp;<span class="id" type="keyword">Import</span> <span class="id" type="var">Imp</span>.<br/>
</div>

<div class="doc">
Recall the original proof of the determinism lemma for the IMP
    language, shown below. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">ceval_deterministic</span>: <span style='font-size:120%;'>&forall;</span><span class="id" type="var">c</span> <span class="id" type="var">st</span> <span class="id" type="var">st<sub>1</sub></span> <span class="id" type="var">st<sub>2</sub></span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">st</span> =[ <span class="id" type="var">c</span> ]⇒ <span class="id" type="var">st<sub>1</sub></span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">st</span> =[ <span class="id" type="var">c</span> ]⇒ <span class="id" type="var">st<sub>2</sub></span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">st<sub>1</sub></span> = <span class="id" type="var">st<sub>2</sub></span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">c</span> <span class="id" type="var">st</span> <span class="id" type="var">st<sub>1</sub></span> <span class="id" type="var">st<sub>2</sub></span> <span class="id" type="var">E<sub>1</sub></span> <span class="id" type="var">E<sub>2</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">generalize</span> <span class="id" type="tactic">dependent</span> <span class="id" type="var">st<sub>2</sub></span>.<br/>
&nbsp;&nbsp;(<span class="id" type="tactic">induction</span> <span class="id" type="var">E<sub>1</sub></span>); <span class="id" type="tactic">intros</span> <span class="id" type="var">st<sub>2</sub></span> <span class="id" type="var">E<sub>2</sub></span>; <span class="id" type="tactic">inversion</span> <span class="id" type="var">E<sub>2</sub></span>; <span class="id" type="tactic">subst</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;E_Skip&nbsp;*)</span> <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;E_Ass&nbsp;*)</span> <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;E_Seq&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">assert</span> (<span class="id" type="var">st'</span> = <span class="id" type="var">st'0</span>) <span class="id" type="keyword">as</span> <span class="id" type="var">EQ<sub>1</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;{ <span class="comment">(*&nbsp;Proof&nbsp;of&nbsp;assertion&nbsp;*)</span> <span class="id" type="tactic">apply</span> <span class="id" type="var">IHE1_1</span>; <span class="id" type="tactic">assumption</span>. }<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">subst</span> <span class="id" type="var">st'0</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">IHE1_2</span>. <span class="id" type="tactic">assumption</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;E_IfTrue&nbsp;*)</span><br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;b<sub>1</sub>&nbsp;reduces&nbsp;to&nbsp;true&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">IHE1</span>. <span class="id" type="tactic">assumption</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;b<sub>1</sub>&nbsp;reduces&nbsp;to&nbsp;false&nbsp;(contradiction)&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">H</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H<sub>5</sub></span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H<sub>5</sub></span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;E_IfFalse&nbsp;*)</span><br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;b<sub>1</sub>&nbsp;reduces&nbsp;to&nbsp;true&nbsp;(contradiction)&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">H</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H<sub>5</sub></span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H<sub>5</sub></span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;b<sub>1</sub>&nbsp;reduces&nbsp;to&nbsp;false&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">IHE1</span>. <span class="id" type="tactic">assumption</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;E_WhileFalse&nbsp;*)</span><br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;b<sub>1</sub>&nbsp;reduces&nbsp;to&nbsp;true&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;b<sub>1</sub>&nbsp;reduces&nbsp;to&nbsp;false&nbsp;(contradiction)&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">H</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H<sub>2</sub></span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H<sub>2</sub></span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;E_WhileTrue&nbsp;*)</span><br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;b<sub>1</sub>&nbsp;reduces&nbsp;to&nbsp;true&nbsp;(contradiction)&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">H</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H<sub>4</sub></span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H<sub>4</sub></span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;b<sub>1</sub>&nbsp;reduces&nbsp;to&nbsp;false&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">assert</span> (<span class="id" type="var">st'</span> = <span class="id" type="var">st'0</span>) <span class="id" type="keyword">as</span> <span class="id" type="var">EQ<sub>1</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;{ <span class="comment">(*&nbsp;Proof&nbsp;of&nbsp;assertion&nbsp;*)</span> <span class="id" type="tactic">apply</span> <span class="id" type="var">IHE1_1</span>; <span class="id" type="tactic">assumption</span>. }<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">subst</span> <span class="id" type="var">st'0</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">IHE1_2</span>. <span class="id" type="tactic">assumption</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
Exercise: rewrite this proof using <span class="inlinecode"><span class="id" type="tactic">auto</span></span> whenever possible.
    (The solution uses <span class="inlinecode"><span class="id" type="tactic">auto</span></span> 9 times.) 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">ceval_deterministic'</span>: <span style='font-size:120%;'>&forall;</span><span class="id" type="var">c</span> <span class="id" type="var">st</span> <span class="id" type="var">st<sub>1</sub></span> <span class="id" type="var">st<sub>2</sub></span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">st</span> =[ <span class="id" type="var">c</span> ]⇒ <span class="id" type="var">st<sub>1</sub></span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">st</span> =[ <span class="id" type="var">c</span> ]⇒ <span class="id" type="var">st<sub>2</sub></span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">st<sub>1</sub></span> = <span class="id" type="var">st<sub>2</sub></span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">admit</span>.<br/>
<span class="id" type="var">Admitted</span>.<br/>
</div>

<div class="doc">
In fact, using automation is not just a matter of calling <span class="inlinecode"><span class="id" type="tactic">auto</span></span>
    in place of one or two other tactics. Using automation is about
    rethinking the organization of sequences of tactics so as to
    minimize the effort involved in writing and maintaining the proof.
    This process is eased by the use of the tactics from
    <span class="inlinecode"><span class="id" type="var">LibTactics.v</span></span>.  So, before trying to optimize the way automation
    is used, let's first rewrite the proof of determinism:

<div class="paragraph"> </div>

<ul class="doclist">
<li> use <span class="inlinecode"><span class="id" type="var">introv</span></span> <span class="inlinecode"><span class="id" type="var">H</span></span> instead of <span class="inlinecode"><span class="id" type="tactic">intros</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode"><span class="id" type="var">H</span></span>,

</li>
<li> use <span class="inlinecode"><span class="id" type="var">gen</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span> instead of <span class="inlinecode"><span class="id" type="tactic">generalize</span></span> <span class="inlinecode"><span class="id" type="tactic">dependent</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span>,

</li>
<li> use <span class="inlinecode"><span class="id" type="var">inverts</span></span> <span class="inlinecode"><span class="id" type="var">H</span></span> instead of <span class="inlinecode"><span class="id" type="tactic">inversion</span></span> <span class="inlinecode"><span class="id" type="var">H</span>;</span> <span class="inlinecode"><span class="id" type="tactic">subst</span></span>,

</li>
<li> use <span class="inlinecode"><span class="id" type="var">tryfalse</span></span> to handle contradictions, and get rid of
        the cases where <span class="inlinecode"><span class="id" type="var">beval</span></span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span class="id" type="var">b<sub>1</sub></span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">true</span></span> and <span class="inlinecode"><span class="id" type="var">beval</span></span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span class="id" type="var">b<sub>1</sub></span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">false</span></span>
        both appear in the context. 
</li>
</ul>

</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">ceval_deterministic''</span>: <span style='font-size:120%;'>&forall;</span><span class="id" type="var">c</span> <span class="id" type="var">st</span> <span class="id" type="var">st<sub>1</sub></span> <span class="id" type="var">st<sub>2</sub></span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">st</span> =[ <span class="id" type="var">c</span> ]⇒ <span class="id" type="var">st<sub>1</sub></span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">st</span> =[ <span class="id" type="var">c</span> ]⇒ <span class="id" type="var">st<sub>2</sub></span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">st<sub>1</sub></span> = <span class="id" type="var">st<sub>2</sub></span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">introv</span> <span class="id" type="var">E<sub>1</sub></span> <span class="id" type="var">E<sub>2</sub></span>. <span class="id" type="var">gen</span> <span class="id" type="var">st<sub>2</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">E<sub>1</sub></span>; <span class="id" type="tactic">intros</span>; <span class="id" type="var">inverts</span> <span class="id" type="var">E<sub>2</sub></span>; <span class="id" type="var">tryfalse</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">auto</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">auto</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">assert</span> (<span class="id" type="var">st'</span> = <span class="id" type="var">st'0</span>). <span class="id" type="tactic">auto</span>. <span class="id" type="tactic">subst</span>. <span class="id" type="tactic">auto</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">auto</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">auto</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">auto</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">assert</span> (<span class="id" type="var">st'</span> = <span class="id" type="var">st'0</span>). <span class="id" type="tactic">auto</span>. <span class="id" type="tactic">subst</span>. <span class="id" type="tactic">auto</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
To obtain a nice clean proof script, we have to remove the calls
    <span class="inlinecode"><span class="id" type="tactic">assert</span></span> <span class="inlinecode">(<span class="id" type="var">st'</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">st'0</span>)</span>. Such a tactic call is not nice
    because it refers to some variables whose name has been
    automatically generated. This kind of tactics tend to be very
    brittle.  The tactic <span class="inlinecode"><span class="id" type="tactic">assert</span></span> <span class="inlinecode">(<span class="id" type="var">st'</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">st'0</span>)</span> is used to assert the
    conclusion that we want to derive from the induction
    hypothesis. So, rather than stating this conclusion explicitly, we
    are going to ask Coq to instantiate the induction hypothesis,
    using automation to figure out how to instantiate it. The tactic
    <span class="inlinecode"><span class="id" type="var">forwards</span></span>, described in <span class="inlinecode"><span class="id" type="var">LibTactics.v</span></span> precisely helps with
    instantiating a fact. So, let's see how it works out on our
    example. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">ceval_deterministic'''</span>: <span style='font-size:120%;'>&forall;</span><span class="id" type="var">c</span> <span class="id" type="var">st</span> <span class="id" type="var">st<sub>1</sub></span> <span class="id" type="var">st<sub>2</sub></span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">st</span> =[ <span class="id" type="var">c</span> ]⇒ <span class="id" type="var">st<sub>1</sub></span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">st</span> =[ <span class="id" type="var">c</span> ]⇒ <span class="id" type="var">st<sub>2</sub></span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">st<sub>1</sub></span> = <span class="id" type="var">st<sub>2</sub></span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;Let's&nbsp;replay&nbsp;the&nbsp;proof&nbsp;up&nbsp;to&nbsp;the&nbsp;<span class="inlinecode"><span class="id" type="tactic">assert</span></span>&nbsp;tactic.&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="var">introv</span> <span class="id" type="var">E<sub>1</sub></span> <span class="id" type="var">E<sub>2</sub></span>. <span class="id" type="var">gen</span> <span class="id" type="var">st<sub>2</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">E<sub>1</sub></span>; <span class="id" type="tactic">intros</span>; <span class="id" type="var">inverts</span> <span class="id" type="var">E<sub>2</sub></span>; <span class="id" type="var">tryfalse</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">auto</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">auto</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;We&nbsp;duplicate&nbsp;the&nbsp;goal&nbsp;for&nbsp;comparing&nbsp;different&nbsp;proofs.&nbsp;*)</span><br/>
&nbsp;&nbsp;- <span class="id" type="var">dup</span> 4.<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;The&nbsp;old&nbsp;proof:&nbsp;*)</span><br/>
&nbsp;&nbsp;+ <span class="id" type="tactic">assert</span> (<span class="id" type="var">st'</span> = <span class="id" type="var">st'0</span>). <span class="id" type="tactic">apply</span> <span class="id" type="var">IHE1_1</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H<sub>1</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;produces&nbsp;<span class="inlinecode"><span class="id" type="var">H</span>:</span> <span class="inlinecode"><span class="id" type="var">st'</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">st'0</span></span>.&nbsp;*)</span> <span class="id" type="var">skip</span>.<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;The&nbsp;new&nbsp;proof,&nbsp;without&nbsp;automation:&nbsp;*)</span><br/>
&nbsp;&nbsp;+ <span class="id" type="var">forwards</span>: <span class="id" type="var">IHE1_1</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H<sub>1</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;produces&nbsp;<span class="inlinecode"><span class="id" type="var">H</span>:</span> <span class="inlinecode"><span class="id" type="var">st'</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">st'0</span></span>.&nbsp;*)</span> <span class="id" type="var">skip</span>.<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;The&nbsp;new&nbsp;proof,&nbsp;with&nbsp;automation:&nbsp;*)</span><br/>
&nbsp;&nbsp;+ <span class="id" type="var">forwards</span>: <span class="id" type="var">IHE1_1</span>. <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;produces&nbsp;<span class="inlinecode"><span class="id" type="var">H</span>:</span> <span class="inlinecode"><span class="id" type="var">st'</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">st'0</span></span>.&nbsp;*)</span> <span class="id" type="var">skip</span>.<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;The&nbsp;new&nbsp;proof,&nbsp;with&nbsp;integrated&nbsp;automation:&nbsp;*)</span><br/>
&nbsp;&nbsp;+ <span class="id" type="var">forwards</span>*: <span class="id" type="var">IHE1_1</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;produces&nbsp;<span class="inlinecode"><span class="id" type="var">H</span>:</span> <span class="inlinecode"><span class="id" type="var">st'</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">st'0</span></span>.&nbsp;*)</span> <span class="id" type="var">skip</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Abort</span>.<br/>
</div>

<div class="doc">
To polish the proof script, it remains to factorize the calls
    to <span class="inlinecode"><span class="id" type="tactic">auto</span></span>, using the star symbol. The proof of determinism can then
    be rewritten in just 4 lines, including no more than 10 tactics. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">ceval_deterministic''''</span>: <span style='font-size:120%;'>&forall;</span><span class="id" type="var">c</span> <span class="id" type="var">st</span> <span class="id" type="var">st<sub>1</sub></span> <span class="id" type="var">st<sub>2</sub></span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">st</span> =[ <span class="id" type="var">c</span> ]⇒ <span class="id" type="var">st<sub>1</sub></span>  →<br/>
&nbsp;&nbsp;<span class="id" type="var">st</span> =[ <span class="id" type="var">c</span> ]⇒ <span class="id" type="var">st<sub>2</sub></span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">st<sub>1</sub></span> = <span class="id" type="var">st<sub>2</sub></span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">introv</span> <span class="id" type="var">E<sub>1</sub></span> <span class="id" type="var">E<sub>2</sub></span>. <span class="id" type="var">gen</span> <span class="id" type="var">st<sub>2</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">E<sub>1</sub></span>; <span class="id" type="tactic">intros</span>; <span class="id" type="var">inverts</span>* <span class="id" type="var">E<sub>2</sub></span>; <span class="id" type="var">tryfalse</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="var">forwards</span>*: <span class="id" type="var">IHE1_1</span>. <span class="id" type="tactic">subst</span>*.<br/>
&nbsp;&nbsp;- <span class="id" type="var">forwards</span>*: <span class="id" type="var">IHE1_1</span>. <span class="id" type="tactic">subst</span>*.<br/>
<span class="id" type="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">End</span> <span class="id" type="var">DeterministicImp</span>.<br/>
</div>

<div class="doc">
<a name="lab560"></a><h2 class="section">Preservation for STLC</h2>

<div class="paragraph"> </div>

 To investigate how to automate the proof of the lemma <span class="inlinecode"><span class="id" type="var">preservation</span></span>,
    let us first import the definitions required to state that lemma. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Set</span> <span class="id" type="var">Warnings</span> "-notation-overridden,-parsing".<br/>
<span class="id" type="var">From</span> <span class="id" type="var">PLF</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">StlcProp</span>.<br/>
<span class="id" type="keyword">Module</span> <span class="id" type="var">PreservationProgressStlc</span>.<br/>
<span class="id" type="keyword">Import</span> <span class="id" type="var">STLC</span>.<br/>
<span class="id" type="keyword">Import</span> <span class="id" type="var">STLCProp</span>.<br/>
</div>

<div class="doc">
Consider the proof of perservation of STLC, shown below.
    This proof already uses <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> through the triple-dot
    mechanism. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">preservation</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">t</span> <span class="id" type="var">t'</span> <span class="id" type="var">T</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">has_type</span> <span class="id" type="var">empty</span> <span class="id" type="var">t</span> <span class="id" type="var">T</span>  →<br/>
&nbsp;&nbsp;<span class="id" type="var">t</span> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> <span class="id" type="var">t'</span>  →<br/>
&nbsp;&nbsp;<span class="id" type="var">has_type</span> <span class="id" type="var">empty</span> <span class="id" type="var">t'</span> <span class="id" type="var">T</span>.<br/>
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">remember</span> (@<span class="id" type="var">empty</span> <span class="id" type="var">ty</span>) <span class="id" type="keyword">as</span> <span class="id" type="var">Gamma</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">t</span> <span class="id" type="var">t'</span> <span class="id" type="var">T</span> <span class="id" type="var">HT</span>. <span class="id" type="tactic">generalize</span> <span class="id" type="tactic">dependent</span> <span class="id" type="var">t'</span>.<br/>
&nbsp;&nbsp;(<span class="id" type="tactic">induction</span> <span class="id" type="var">HT</span>); <span class="id" type="tactic">intros</span> <span class="id" type="var">t'</span> <span class="id" type="var">HE</span>; <span class="id" type="tactic">subst</span> <span class="id" type="var">Gamma</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_Var&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">HE</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_Abs&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">HE</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_App&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">HE</span>; <span class="id" type="tactic">subst</span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;The&nbsp;ST_App1&nbsp;and&nbsp;ST_App2&nbsp;cases&nbsp;are&nbsp;immediate&nbsp;by&nbsp;induction,&nbsp;and<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;auto&nbsp;takes&nbsp;care&nbsp;of&nbsp;them&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;ST_AppAbs&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">substitution_preserves_typing</span> <span class="id" type="keyword">with</span> <span class="id" type="var">T<sub>11</sub></span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">HT<sub>1</sub></span>...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_True&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">HE</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_False&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">HE</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_If&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">HE</span>; <span class="id" type="tactic">subst</span>...<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
Exercise: rewrite this proof using tactics from <span class="inlinecode"><span class="id" type="var">LibTactics</span></span>
    and calling automation using the star symbol rather than the
    triple-dot notation. More precisely, make use of the tactics
    <span class="inlinecode"><span class="id" type="var">inverts</span>*</span> and <span class="inlinecode"><span class="id" type="var">applys</span>*</span> to call <span class="inlinecode"><span class="id" type="tactic">auto</span>*</span> after a call to
    <span class="inlinecode"><span class="id" type="var">inverts</span></span> or to <span class="inlinecode"><span class="id" type="var">applys</span></span>. The solution is three lines long. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">preservation'</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">t</span> <span class="id" type="var">t'</span> <span class="id" type="var">T</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">has_type</span> <span class="id" type="var">empty</span> <span class="id" type="var">t</span> <span class="id" type="var">T</span>  →<br/>
&nbsp;&nbsp;<span class="id" type="var">t</span> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> <span class="id" type="var">t'</span>  →<br/>
&nbsp;&nbsp;<span class="id" type="var">has_type</span> <span class="id" type="var">empty</span> <span class="id" type="var">t'</span> <span class="id" type="var">T</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">admit</span>.<br/>
<span class="id" type="var">Admitted</span>.<br/>
</div>

<div class="doc">
<a name="lab561"></a><h2 class="section">Progress for STLC</h2>

<div class="paragraph"> </div>

 Consider the proof of the progress theorem. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="tactic">progress</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">t</span> <span class="id" type="var">T</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">has_type</span> <span class="id" type="var">empty</span> <span class="id" type="var">t</span> <span class="id" type="var">T</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">value</span> <span class="id" type="var">t</span> ∨ <span style='font-size:120%;'>&exist;</span><span class="id" type="var">t'</span>, <span class="id" type="var">t</span> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> <span class="id" type="var">t'</span>.<br/>
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">t</span> <span class="id" type="var">T</span> <span class="id" type="var">Ht</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">remember</span> (@<span class="id" type="var">empty</span> <span class="id" type="var">ty</span>) <span class="id" type="keyword">as</span> <span class="id" type="var">Gamma</span>.<br/>
&nbsp;&nbsp;(<span class="id" type="tactic">induction</span> <span class="id" type="var">Ht</span>); <span class="id" type="tactic">subst</span> <span class="id" type="var">Gamma</span>...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_Var&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_App&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">right</span>. <span class="id" type="tactic">destruct</span> <span class="id" type="var">IHHt1</span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;t<sub>1</sub>&nbsp;is&nbsp;a&nbsp;value&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">IHHt2</span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;* <span class="comment">(*&nbsp;t<sub>2</sub>&nbsp;is&nbsp;a&nbsp;value&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>; <span class="id" type="tactic">subst</span>; <span class="id" type="tactic">try</span> <span class="id" type="var">solve_by_invert</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span>([<span class="id" type="var">x<sub>0</sub></span>:=<span class="id" type="var">t<sub>2</sub></span>]<span class="id" type="var">t</span>)...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;* <span class="comment">(*&nbsp;t<sub>2</sub>&nbsp;steps&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">H<sub>0</sub></span> <span class="id" type="keyword">as</span> [<span class="id" type="var">t<sub>2</sub>'</span> <span class="id" type="var">Hstp</span>]. <span style='font-size:120%;'>&exist;</span>(<span class="id" type="var">app</span> <span class="id" type="var">t<sub>1</sub></span> <span class="id" type="var">t<sub>2</sub>'</span>)...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;t<sub>1</sub>&nbsp;steps&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">H</span> <span class="id" type="keyword">as</span> [<span class="id" type="var">t<sub>1</sub>'</span> <span class="id" type="var">Hstp</span>]. <span style='font-size:120%;'>&exist;</span>(<span class="id" type="var">app</span> <span class="id" type="var">t<sub>1</sub>'</span> <span class="id" type="var">t<sub>2</sub></span>)...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_If&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">right</span>. <span class="id" type="tactic">destruct</span> <span class="id" type="var">IHHt1</span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">t<sub>1</sub></span>; <span class="id" type="tactic">try</span> <span class="id" type="var">solve_by_invert</span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>. <span style='font-size:120%;'>&exist;</span>(<span class="id" type="var">test</span> <span class="id" type="var">x<sub>0</sub></span> <span class="id" type="var">t<sub>2</sub></span> <span class="id" type="var">t<sub>3</sub></span>)...<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
Exercise: optimize the above proof.
    Hint: make use of <span class="inlinecode"><span class="id" type="tactic">destruct</span>*</span> and <span class="inlinecode"><span class="id" type="var">inverts</span>*</span>.
    The solution fits on 10 short lines. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">progress'</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">t</span> <span class="id" type="var">T</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">has_type</span> <span class="id" type="var">empty</span> <span class="id" type="var">t</span> <span class="id" type="var">T</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">value</span> <span class="id" type="var">t</span> ∨ <span style='font-size:120%;'>&exist;</span><span class="id" type="var">t'</span>, <span class="id" type="var">t</span> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> <span class="id" type="var">t'</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">admit</span>.<br/>
<span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">End</span> <span class="id" type="var">PreservationProgressStlc</span>.<br/>
</div>

<div class="doc">
<a name="lab562"></a><h2 class="section">BigStep and SmallStep</h2>

</div>
<div class="code code-space">

<br/>
<span class="id" type="var">From</span> <span class="id" type="var">PLF</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Smallstep</span>.<br/>
<span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Program</span>.<br/>
<span class="id" type="keyword">Module</span> <span class="id" type="var">Semantics</span>.<br/>
</div>

<div class="doc">
Consider the proof relating a small-step reduction judgment
    to a big-step reduction judgment. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">multistep__eval</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">t</span> <span class="id" type="var">v</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">normal_form_of</span> <span class="id" type="var">t</span> <span class="id" type="var">v</span> → <span style='font-size:120%;'>&exist;</span><span class="id" type="var">n</span>, <span class="id" type="var">v</span> = <span class="id" type="var">C</span> <span class="id" type="var">n</span> ∧ <span class="id" type="var">t</span> ==&gt; <span class="id" type="var">n</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">t</span> <span class="id" type="var">v</span> <span class="id" type="var">Hnorm</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">normal_form_of</span> <span class="id" type="keyword">in</span> <span class="id" type="var">Hnorm</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">Hnorm</span> <span class="id" type="keyword">as</span> [<span class="id" type="var">Hs</span> <span class="id" type="var">Hnf</span>]; <span class="id" type="tactic">clear</span> <span class="id" type="var">Hnorm</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">nf_same_as_value</span> <span class="id" type="keyword">in</span> <span class="id" type="var">Hnf</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">Hnf</span>. <span class="id" type="tactic">clear</span> <span class="id" type="var">Hnf</span>.<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">n</span>. <span class="id" type="tactic">split</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">Hs</span>; <span class="id" type="tactic">subst</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;multi_refl&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">E_Const</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;multi_step&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">eapply</span> <span class="id" type="var">step__eval</span>. <span class="id" type="var">eassumption</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">IHHs</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
Our goal is to optimize the above proof. It is generally
    easier to isolate inductions into separate lemmas. So,
    we are going to first prove an intermediate result
    that consists of the judgment over which the induction
    is being performed. 
<div class="paragraph"> </div>

 Exercise: prove the following result, using tactics
    <span class="inlinecode"><span class="id" type="var">introv</span></span>, <span class="inlinecode"><span class="id" type="tactic">induction</span></span> and <span class="inlinecode"><span class="id" type="tactic">subst</span></span>, and <span class="inlinecode"><span class="id" type="tactic">apply</span>*</span>.
    The solution fits on 3 short lines. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">multistep_eval_ind</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">t</span> <span class="id" type="var">v</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">t</span> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span><span style='letter-spacing:-.2em;'>&gt;</span><span style='vertical-align:15%;'>*</span></span></span> <span class="id" type="var">v</span> → <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>, <span class="id" type="var">C</span> <span class="id" type="var">n</span> = <span class="id" type="var">v</span> → <span class="id" type="var">t</span> ==&gt; <span class="id" type="var">n</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">admit</span>.<br/>
<span class="id" type="var">Admitted</span>.<br/>
</div>

<div class="doc">
Exercise: using the lemma above, simplify the proof of
    the result <span class="inlinecode"><span class="id" type="var">multistep__eval</span></span>. You should use the tactics
    <span class="inlinecode"><span class="id" type="var">introv</span></span>, <span class="inlinecode"><span class="id" type="var">inverts</span></span>, <span class="inlinecode"><span class="id" type="tactic">split</span>*</span> and <span class="inlinecode"><span class="id" type="tactic">apply</span>*</span>.
    The solution fits on 2 lines. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">multistep__eval'</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">t</span> <span class="id" type="var">v</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">normal_form_of</span> <span class="id" type="var">t</span> <span class="id" type="var">v</span> → <span style='font-size:120%;'>&exist;</span><span class="id" type="var">n</span>, <span class="id" type="var">v</span> = <span class="id" type="var">C</span> <span class="id" type="var">n</span> ∧ <span class="id" type="var">t</span> ==&gt; <span class="id" type="var">n</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">admit</span>.<br/>
<span class="id" type="var">Admitted</span>.<br/>
</div>

<div class="doc">
If we try to combine the two proofs into a single one,
    we will likely fail, because of a limitation of the
    <span class="inlinecode"><span class="id" type="tactic">induction</span></span> tactic. Indeed, this tactic loses
    information when applied to a property whose arguments
    are not reduced to variables, such as <span class="inlinecode"><span class="id" type="var">t</span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span><span style='letter-spacing:-.2em;'>&gt;</span><span style='vertical-align:15%;'>*</span></span></span></span> <span class="inlinecode">(<span class="id" type="var">C</span></span> <span class="inlinecode"><span class="id" type="var">n</span>)</span>.
    You will thus need to use the more powerful tactic called
    <span class="inlinecode"><span class="id" type="tactic">dependent</span></span> <span class="inlinecode"><span class="id" type="tactic">induction</span></span>. (This tactic is available only after
    importing the <span class="inlinecode"><span class="id" type="var">Program</span></span> library, as we did above.) 
<div class="paragraph"> </div>

 Exercise: prove the lemma <span class="inlinecode"><span class="id" type="var">multistep__eval</span></span> without invoking
    the lemma <span class="inlinecode"><span class="id" type="var">multistep_eval_ind</span></span>, that is, by inlining the proof
    by induction involved in <span class="inlinecode"><span class="id" type="var">multistep_eval_ind</span></span>, using the
    tactic <span class="inlinecode"><span class="id" type="tactic">dependent</span></span> <span class="inlinecode"><span class="id" type="tactic">induction</span></span> instead of <span class="inlinecode"><span class="id" type="tactic">induction</span></span>.
    The solution fits on 6 lines. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">multistep__eval''</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">t</span> <span class="id" type="var">v</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">normal_form_of</span> <span class="id" type="var">t</span> <span class="id" type="var">v</span> → <span style='font-size:120%;'>&exist;</span><span class="id" type="var">n</span>, <span class="id" type="var">v</span> = <span class="id" type="var">C</span> <span class="id" type="var">n</span> ∧ <span class="id" type="var">t</span> ==&gt; <span class="id" type="var">n</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">admit</span>.<br/>
<span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">End</span> <span class="id" type="var">Semantics</span>.<br/>
</div>

<div class="doc">
<a name="lab563"></a><h2 class="section">Preservation for STLCRef</h2>

</div>
<div class="code code-space">

<br/>
<span class="id" type="var">From</span> <span class="id" type="var">Coq</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">omega.Omega</span>.<br/>
<span class="id" type="var">From</span> <span class="id" type="var">PLF</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">References</span>.<br/>
<span class="id" type="keyword">Import</span> <span class="id" type="var">STLCRef</span>.<br/>
<span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Program</span>.<br/>
<span class="id" type="keyword">Module</span> <span class="id" type="var">PreservationProgressReferences</span>.<br/>
<span class="id" type="keyword">Hint</span> <span class="id" type="keyword">Resolve</span> <span class="id" type="var">store_weakening</span> <span class="id" type="var">extends_refl</span>.<br/>
</div>

<div class="doc">
The proof of preservation for <span class="inlinecode"><span class="id" type="var">STLCRef</span></span> can be found in chapter
    <span class="inlinecode"><span class="id" type="var">References</span></span>.  The optimized proof script is more than twice
    shorter.  The following material explains how to build the
    optimized proof script.  The resulting optimized proof script for
    the preservation theorem appears afterwards. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">preservation</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">ST</span> <span class="id" type="var">t</span> <span class="id" type="var">t'</span> <span class="id" type="var">T</span> <span class="id" type="var">st</span> <span class="id" type="var">st'</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">has_type</span> <span class="id" type="var">empty</span> <span class="id" type="var">ST</span> <span class="id" type="var">t</span> <span class="id" type="var">T</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">store_well_typed</span> <span class="id" type="var">ST</span> <span class="id" type="var">st</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">t</span> / <span class="id" type="var">st</span> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> <span class="id" type="var">t'</span> / <span class="id" type="var">st'</span> →<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">ST'</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">extends</span> <span class="id" type="var">ST'</span> <span class="id" type="var">ST</span> ∧<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">has_type</span> <span class="id" type="var">empty</span> <span class="id" type="var">ST'</span> <span class="id" type="var">t'</span> <span class="id" type="var">T</span> ∧<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">store_well_typed</span> <span class="id" type="var">ST'</span> <span class="id" type="var">st'</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;old:&nbsp;<span class="inlinecode"><span class="id" type="keyword">Proof</span>.</span> <span class="inlinecode"><span class="id" type="keyword">with</span></span> <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> <span class="inlinecode"><span class="id" type="keyword">using</span></span> <span class="inlinecode"><span class="id" type="var">store_weakening</span>,</span> <span class="inlinecode"><span class="id" type="var">extends_refl</span>.</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;new:&nbsp;<span class="inlinecode"><span class="id" type="keyword">Proof</span>.</span>,&nbsp;and&nbsp;the&nbsp;two&nbsp;lemmas&nbsp;are&nbsp;registered&nbsp;as&nbsp;hints<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;before&nbsp;the&nbsp;proof&nbsp;of&nbsp;the&nbsp;lemma,&nbsp;possibly&nbsp;inside&nbsp;a&nbsp;section&nbsp;in<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;order&nbsp;to&nbsp;restrict&nbsp;the&nbsp;scope&nbsp;of&nbsp;the&nbsp;hints.&nbsp;*)</span><br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;<span class="id" type="var">remember</span> (@<span class="id" type="var">empty</span> <span class="id" type="var">ty</span>) <span class="id" type="keyword">as</span> <span class="id" type="var">Gamma</span>. <span class="id" type="var">introv</span> <span class="id" type="var">Ht</span>. <span class="id" type="var">gen</span> <span class="id" type="var">t'</span>.<br/>
&nbsp;&nbsp;(<span class="id" type="tactic">induction</span> <span class="id" type="var">Ht</span>); <span class="id" type="var">introv</span> <span class="id" type="var">HST</span> <span class="id" type="var">Hstep</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;old:&nbsp;<span class="inlinecode"><span class="id" type="tactic">subst</span>;</span> <span class="inlinecode"><span class="id" type="tactic">try</span></span> <span class="inlinecode"><span class="id" type="var">solve_by_invert</span>;</span> <span class="inlinecode"><span class="id" type="tactic">inversion</span></span> <span class="inlinecode"><span class="id" type="var">Hstep</span>;</span> <span class="inlinecode"><span class="id" type="tactic">subst</span>;</span>
             <span class="inlinecode"><span class="id" type="tactic">try</span></span> <span class="inlinecode">(<span class="id" type="tactic">eauto</span></span> <span class="inlinecode"><span class="id" type="keyword">using</span></span> <span class="inlinecode"><span class="id" type="var">store_weakening</span>,</span> <span class="inlinecode"><span class="id" type="var">extends_refl</span>)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;new:&nbsp;<span class="inlinecode"><span class="id" type="tactic">subst</span></span> <span class="inlinecode"><span class="id" type="var">Gamma</span>;</span> <span class="inlinecode"><span class="id" type="var">inverts</span></span> <span class="inlinecode"><span class="id" type="var">Hstep</span>;</span> <span class="inlinecode"><span class="id" type="tactic">eauto</span>.</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;We&nbsp;want&nbsp;to&nbsp;be&nbsp;more&nbsp;precise&nbsp;on&nbsp;what&nbsp;exactly&nbsp;we&nbsp;substitute,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;and&nbsp;we&nbsp;do&nbsp;not&nbsp;want&nbsp;to&nbsp;call&nbsp;<span class="inlinecode"><span class="id" type="tactic">try</span></span> <span class="inlinecode"><span class="id" type="var">solve_by_invert</span></span>&nbsp;which<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;is&nbsp;way&nbsp;to&nbsp;slow.&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">subst</span> <span class="id" type="var">Gamma</span>; <span class="id" type="var">inverts</span> <span class="id" type="var">Hstep</span>; <span class="id" type="tactic">eauto</span>.<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;T_App&nbsp;*)</span><br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;ST_AppAbs&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;old:<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;exists&nbsp;ST.&nbsp;inversion&nbsp;Ht<sub>1</sub>;&nbsp;subst.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;split;&nbsp;try&nbsp;split...&nbsp;eapply&nbsp;substitution_preserves_typing...&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;new:&nbsp;we&nbsp;use&nbsp;<span class="inlinecode"><span class="id" type="var">inverts</span></span>&nbsp;in&nbsp;place&nbsp;of&nbsp;<span class="inlinecode"><span class="id" type="tactic">inversion</span></span>&nbsp;and&nbsp;<span class="inlinecode"><span class="id" type="var">splits</span></span>&nbsp;to<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;split&nbsp;the&nbsp;conjunction,&nbsp;and&nbsp;<span class="inlinecode"><span class="id" type="var">applys</span>*</span>&nbsp;in&nbsp;place&nbsp;of&nbsp;<span class="inlinecode"><span class="id" type="tactic">eapply</span>...</span>&nbsp;*)</span><br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">ST</span>. <span class="id" type="var">inverts</span> <span class="id" type="var">Ht<sub>1</sub></span>. <span class="id" type="var">splits</span>*. <span class="id" type="var">applys</span>* <span class="id" type="var">substitution_preserves_typing</span>.<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;ST_App1&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;old:<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;eapply&nbsp;IHHt1&nbsp;in&nbsp;H<sub>0</sub>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;inversion&nbsp;H<sub>0</sub>&nbsp;as&nbsp;<span class="inlinecode"><span class="id" type="var">ST'</span></span> <span class="inlinecode">[<span class="id" type="var">Hext</span></span> <span class="inlinecode">[<span class="id" type="var">Hty</span></span> <span class="inlinecode"><span class="id" type="var">Hsty</span>]]</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;exists&nbsp;ST'...&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;new:&nbsp;The&nbsp;tactic&nbsp;<span class="inlinecode"><span class="id" type="tactic">eapply</span></span> <span class="inlinecode"><span class="id" type="var">IHHt1</span></span> <span class="inlinecode"><span class="id" type="keyword">in</span></span> <span class="inlinecode"><span class="id" type="var">H<sub>0</sub></span>...</span>&nbsp;applies&nbsp;<span class="inlinecode"><span class="id" type="var">IHHt1</span></span>&nbsp;to&nbsp;<span class="inlinecode"><span class="id" type="var">H<sub>0</sub></span></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;But&nbsp;<span class="inlinecode"><span class="id" type="var">H<sub>0</sub></span></span>&nbsp;is&nbsp;only&nbsp;thing&nbsp;that&nbsp;<span class="inlinecode"><span class="id" type="var">IHHt1</span></span>&nbsp;could&nbsp;be&nbsp;applied&nbsp;to,&nbsp;so<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;there&nbsp;<span class="inlinecode"><span class="id" type="tactic">eauto</span></span>&nbsp;can&nbsp;figure&nbsp;this&nbsp;out&nbsp;on&nbsp;its&nbsp;own.&nbsp;The&nbsp;tactic<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" type="var">forwards</span></span>&nbsp;is&nbsp;used&nbsp;to&nbsp;instantiate&nbsp;all&nbsp;the&nbsp;arguments&nbsp;of&nbsp;<span class="inlinecode"><span class="id" type="var">IHHt1</span></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;producing&nbsp;existential&nbsp;variables&nbsp;and&nbsp;subgoals&nbsp;when&nbsp;needed.&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="var">forwards</span>: <span class="id" type="var">IHHt1</span>. <span class="id" type="tactic">eauto</span>. <span class="id" type="tactic">eauto</span>. <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;At&nbsp;this&nbsp;point,&nbsp;we&nbsp;need&nbsp;to&nbsp;decompose&nbsp;the&nbsp;hypothesis&nbsp;<span class="inlinecode"><span class="id" type="var">H</span></span>&nbsp;that&nbsp;has<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;just&nbsp;been&nbsp;created&nbsp;by&nbsp;<span class="inlinecode"><span class="id" type="var">forwards</span></span>.&nbsp;This&nbsp;is&nbsp;done&nbsp;by&nbsp;the&nbsp;first&nbsp;part<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;of&nbsp;the&nbsp;preprocessing&nbsp;phase&nbsp;of&nbsp;<span class="inlinecode"><span class="id" type="var">jauto</span></span>.&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="var">jauto_set_hyps</span>; <span class="id" type="tactic">intros</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;It&nbsp;remains&nbsp;to&nbsp;decompose&nbsp;the&nbsp;goal,&nbsp;which&nbsp;is&nbsp;done&nbsp;by&nbsp;the&nbsp;second<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;part&nbsp;of&nbsp;the&nbsp;preprocessing&nbsp;phase&nbsp;of&nbsp;<span class="inlinecode"><span class="id" type="var">jauto</span></span>.&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="var">jauto_set_goal</span>; <span class="id" type="tactic">intros</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;All&nbsp;the&nbsp;subgoals&nbsp;produced&nbsp;can&nbsp;then&nbsp;be&nbsp;solved&nbsp;by&nbsp;<span class="inlinecode"><span class="id" type="tactic">eauto</span></span>.&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="tactic">eauto</span>. <span class="id" type="tactic">eauto</span>. <span class="id" type="tactic">eauto</span>.<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;-(* <span class="id" type="var">ST_App2</span> *)<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;old:<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;eapply&nbsp;IHHt2&nbsp;in&nbsp;H<sub>5</sub>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;inversion&nbsp;H<sub>5</sub>&nbsp;as&nbsp;<span class="inlinecode"><span class="id" type="var">ST'</span></span> <span class="inlinecode">[<span class="id" type="var">Hext</span></span> <span class="inlinecode">[<span class="id" type="var">Hty</span></span> <span class="inlinecode"><span class="id" type="var">Hsty</span>]]</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;exists&nbsp;ST'...&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;new:&nbsp;this&nbsp;time,&nbsp;we&nbsp;need&nbsp;to&nbsp;call&nbsp;<span class="inlinecode"><span class="id" type="var">forwards</span></span>&nbsp;on&nbsp;<span class="inlinecode"><span class="id" type="var">IHHt2</span></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;and&nbsp;we&nbsp;call&nbsp;<span class="inlinecode"><span class="id" type="var">jauto</span></span>&nbsp;right&nbsp;away,&nbsp;by&nbsp;writing&nbsp;<span class="inlinecode"><span class="id" type="var">forwards</span>*</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;proving&nbsp;the&nbsp;goal&nbsp;in&nbsp;a&nbsp;single&nbsp;tactic!&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="var">forwards</span>*: <span class="id" type="var">IHHt2</span>.<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;The&nbsp;same&nbsp;trick&nbsp;works&nbsp;for&nbsp;many&nbsp;of&nbsp;the&nbsp;other&nbsp;subgoals.&nbsp;*)</span><br/>
&nbsp;&nbsp;- <span class="id" type="var">forwards</span>*: <span class="id" type="var">IHHt</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="var">forwards</span>*: <span class="id" type="var">IHHt</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="var">forwards</span>*: <span class="id" type="var">IHHt1</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="var">forwards</span>*: <span class="id" type="var">IHHt2</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="var">forwards</span>*: <span class="id" type="var">IHHt1</span>.<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_Ref&nbsp;*)</span><br/>
&nbsp;&nbsp;+ <span class="comment">(*&nbsp;ST_RefValue&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;old:<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;exists&nbsp;(ST&nbsp;++&nbsp;T<sub>1</sub>::nil).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;inversion&nbsp;HST;&nbsp;subst.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;split.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;apply&nbsp;extends_app.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;split.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;replace&nbsp;(TRef&nbsp;T<sub>1</sub>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;with&nbsp;(TRef&nbsp;(store_Tlookup&nbsp;(length&nbsp;st)&nbsp;(ST&nbsp;++&nbsp;T<sub>1</sub>::nil))).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;apply&nbsp;T_Loc.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;rewrite&nbsp;&lt;-&nbsp;H.&nbsp;rewrite&nbsp;app_length,&nbsp;plus_comm.&nbsp;simpl.&nbsp;omega.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;unfold&nbsp;store_Tlookup.&nbsp;rewrite&nbsp;&lt;-&nbsp;H.&nbsp;rewrite&nbsp;app_nth2;&nbsp;try&nbsp;omega.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;rewrite&nbsp;minus_diag.&nbsp;simpl.&nbsp;reflexivity.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;apply&nbsp;store_well_typed_app;&nbsp;assumption.&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;new:&nbsp;In&nbsp;this&nbsp;proof&nbsp;case,&nbsp;we&nbsp;need&nbsp;to&nbsp;perform&nbsp;an&nbsp;inversion<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;without&nbsp;removing&nbsp;the&nbsp;hypothesis.&nbsp;The&nbsp;tactic&nbsp;<span class="inlinecode"><span class="id" type="var">inverts</span></span> <span class="inlinecode"><span class="id" type="var">keep</span></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;serves&nbsp;exactly&nbsp;this&nbsp;purpose.&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span>(<span class="id" type="var">ST</span> ++ <span class="id" type="var">T<sub>1</sub></span>::<span class="id" type="var">nil</span>). <span class="id" type="var">inverts</span> <span class="id" type="var">keep</span> <span class="id" type="var">HST</span>. <span class="id" type="var">splits</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;The&nbsp;proof&nbsp;of&nbsp;the&nbsp;first&nbsp;subgoal&nbsp;needs&nbsp;no&nbsp;change&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">extends_app</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;For&nbsp;the&nbsp;second&nbsp;subgoal,&nbsp;we&nbsp;use&nbsp;the&nbsp;tactic&nbsp;<span class="inlinecode"><span class="id" type="var">applys_eq</span></span>&nbsp;to&nbsp;avoid<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;a&nbsp;manual&nbsp;<span class="inlinecode"><span class="id" type="tactic">replace</span></span>&nbsp;before&nbsp;<span class="inlinecode"><span class="id" type="var">T_loc</span></span>&nbsp;can&nbsp;be&nbsp;applied.&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">applys_eq</span> <span class="id" type="var">T_Loc</span> 1.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;To&nbsp;justify&nbsp;the&nbsp;inequality,&nbsp;there&nbsp;is&nbsp;no&nbsp;need&nbsp;to&nbsp;call&nbsp;<span class="inlinecode"><span class="id" type="tactic">rewrite</span></span> <span class="inlinecode">&lt;-</span> <span class="inlinecode"><span class="id" type="var">H</span></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;because&nbsp;the&nbsp;tactic&nbsp;<span class="inlinecode"><span class="id" type="tactic">omega</span></span>&nbsp;is&nbsp;able&nbsp;to&nbsp;exploit&nbsp;<span class="inlinecode"><span class="id" type="var">H</span></span>&nbsp;on&nbsp;its&nbsp;own.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;So,&nbsp;only&nbsp;the&nbsp;rewriting&nbsp;of&nbsp;<span class="inlinecode"><span class="id" type="var">app_length</span></span>&nbsp;and&nbsp;the&nbsp;call&nbsp;to&nbsp;the<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;tactic&nbsp;<span class="inlinecode"><span class="id" type="tactic">omega</span></span>&nbsp;remain,&nbsp;with&nbsp;a&nbsp;call&nbsp;to&nbsp;<span class="inlinecode"><span class="id" type="tactic">simpl</span></span>&nbsp;to&nbsp;unfold&nbsp;the<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;definition&nbsp;of&nbsp;<span class="inlinecode"><span class="id" type="var">app</span></span>.&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">app_length</span>. <span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">omega</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;The&nbsp;next&nbsp;proof&nbsp;case&nbsp;is&nbsp;hard&nbsp;to&nbsp;polish&nbsp;because&nbsp;it&nbsp;relies&nbsp;on&nbsp;the<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;lemma&nbsp;<span class="inlinecode"><span class="id" type="var">app_nth1</span></span>&nbsp;whose&nbsp;statement&nbsp;is&nbsp;not&nbsp;automation-friendly.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;We'll&nbsp;come&nbsp;back&nbsp;to&nbsp;this&nbsp;proof&nbsp;case&nbsp;further&nbsp;on.&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">store_Tlookup</span>. <span class="id" type="tactic">rewrite</span> &lt;- <span class="id" type="var">H</span>. <span class="id" type="tactic">rewrite</span>* <span class="id" type="var">app_nth2</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;Last,&nbsp;we&nbsp;replace&nbsp;<span class="inlinecode"><span class="id" type="tactic">apply</span></span> <span class="inlinecode">..;</span> <span class="inlinecode"><span class="id" type="tactic">assumption</span></span>&nbsp;with&nbsp;<span class="inlinecode"><span class="id" type="tactic">apply</span>*</span> <span class="inlinecode">..</span>&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">minus_diag</span>. <span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span>* <span class="id" type="var">store_well_typed_app</span>.<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;- <span class="id" type="var">forwards</span>*: <span class="id" type="var">IHHt</span>.<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_Deref&nbsp;*)</span><br/>
&nbsp;&nbsp;+ <span class="comment">(*&nbsp;ST_DerefLoc&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;old:<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;exists&nbsp;ST.&nbsp;split;&nbsp;try&nbsp;split...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;destruct&nbsp;HST&nbsp;as&nbsp;<span class="inlinecode"><span class="id" type="var">_</span></span> <span class="inlinecode"><span class="id" type="var">Hsty</span></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;replace&nbsp;T<sub>11</sub>&nbsp;with&nbsp;(store_Tlookup&nbsp;l&nbsp;ST).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;apply&nbsp;Hsty...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;inversion&nbsp;Ht;&nbsp;subst...&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;new:&nbsp;we&nbsp;start&nbsp;by&nbsp;calling&nbsp;<span class="inlinecode"><span style='font-size:120%;'>&exist;</span></span> <span class="inlinecode"><span class="id" type="var">ST</span></span>&nbsp;and&nbsp;<span class="inlinecode"><span class="id" type="var">splits</span>*</span>.&nbsp;*)</span><br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">ST</span>. <span class="id" type="var">splits</span>*.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;new:&nbsp;we&nbsp;replace&nbsp;<span class="inlinecode"><span class="id" type="tactic">destruct</span></span> <span class="inlinecode"><span class="id" type="var">HST</span></span> <span class="inlinecode"><span class="id" type="keyword">as</span></span> <span class="inlinecode">[<span class="id" type="var">_</span></span> <span class="inlinecode"><span class="id" type="var">Hsty</span>]</span>&nbsp;by&nbsp;the&nbsp;following&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="var">lets</span> [<span class="id" type="var">_</span> <span class="id" type="var">Hsty</span>]: <span class="id" type="var">HST</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;new:&nbsp;then&nbsp;we&nbsp;use&nbsp;the&nbsp;tactic&nbsp;<span class="inlinecode"><span class="id" type="var">applys_eq</span></span>&nbsp;to&nbsp;avoid&nbsp;the&nbsp;need&nbsp;to<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;perform&nbsp;a&nbsp;manual&nbsp;<span class="inlinecode"><span class="id" type="tactic">replace</span></span>&nbsp;before&nbsp;applying&nbsp;<span class="inlinecode"><span class="id" type="var">Hsty</span></span>.&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="var">applys_eq</span>* <span class="id" type="var">Hsty</span> 1.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;new:&nbsp;we&nbsp;then&nbsp;can&nbsp;call&nbsp;<span class="inlinecode"><span class="id" type="var">inverts</span></span>&nbsp;in&nbsp;place&nbsp;of&nbsp;<span class="inlinecode"><span class="id" type="tactic">inversion</span>;<span class="id" type="tactic">subst</span></span>&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="var">inverts</span>* <span class="id" type="var">Ht</span>.<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;- <span class="id" type="var">forwards</span>*: <span class="id" type="var">IHHt</span>.<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_Assign&nbsp;*)</span><br/>
&nbsp;&nbsp;+ <span class="comment">(*&nbsp;ST_Assign&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;old:<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;exists&nbsp;ST.&nbsp;split;&nbsp;try&nbsp;split...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;eapply&nbsp;assign_pres_store_typing...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;inversion&nbsp;Ht<sub>1</sub>;&nbsp;subst...&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;new:&nbsp;simply&nbsp;using&nbsp;nicer&nbsp;tactics&nbsp;*)</span><br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">ST</span>. <span class="id" type="var">splits</span>*. <span class="id" type="var">applys</span>* <span class="id" type="var">assign_pres_store_typing</span>. <span class="id" type="var">inverts</span>* <span class="id" type="var">Ht<sub>1</sub></span>.<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;- <span class="id" type="var">forwards</span>*: <span class="id" type="var">IHHt1</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="var">forwards</span>*: <span class="id" type="var">IHHt2</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
Let's come back to the proof case that was hard to optimize.
    The difficulty comes from the statement of <span class="inlinecode"><span class="id" type="var">nth_eq_last</span></span>, which
    takes the form <span class="inlinecode"><span class="id" type="var">nth</span></span> <span class="inlinecode">(<span class="id" type="var">length</span></span> <span class="inlinecode"><span class="id" type="var">l</span>)</span> <span class="inlinecode">(<span class="id" type="var">l</span></span> <span class="inlinecode">++</span> <span class="inlinecode"><span class="id" type="var">x</span>::<span class="id" type="var">nil</span>)</span> <span class="inlinecode"><span class="id" type="var">d</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">x</span></span>. This lemma is
    hard to exploit because its first argument, <span class="inlinecode"><span class="id" type="var">length</span></span> <span class="inlinecode"><span class="id" type="var">l</span></span>, mentions
    a list <span class="inlinecode"><span class="id" type="var">l</span></span> that has to be exactly the same as the <span class="inlinecode"><span class="id" type="var">l</span></span> occuring in
    <span class="inlinecode"><span class="id" type="var">l</span></span> <span class="inlinecode">++</span> <span class="inlinecode"><span class="id" type="var">x</span>::<span class="id" type="var">nil</span></span>. In practice, the first argument is often a natural
    number <span class="inlinecode"><span class="id" type="var">n</span></span> that is provably equal to <span class="inlinecode"><span class="id" type="var">length</span></span> <span class="inlinecode"><span class="id" type="var">l</span></span> yet that is not
    syntactically equal to <span class="inlinecode"><span class="id" type="var">length</span></span> <span class="inlinecode"><span class="id" type="var">l</span></span>. There is a simple fix for
    making <span class="inlinecode"><span class="id" type="var">nth_eq_last</span></span> easy to apply: introduce the intermediate
    variable <span class="inlinecode"><span class="id" type="var">n</span></span> explicitly, so that the goal becomes
    <span class="inlinecode"><span class="id" type="var">nth</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">(<span class="id" type="var">l</span></span> <span class="inlinecode">++</span> <span class="inlinecode"><span class="id" type="var">x</span>::<span class="id" type="var">nil</span>)</span> <span class="inlinecode"><span class="id" type="var">d</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">x</span></span>, with a premise asserting <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">length</span></span> <span class="inlinecode"><span class="id" type="var">l</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">nth_eq_last'</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">A</span> : <span class="id" type="keyword">Type</span>) (<span class="id" type="var">l</span> : <span class="id" type="var">list</span> <span class="id" type="var">A</span>) (<span class="id" type="var">x</span> <span class="id" type="var">d</span> : <span class="id" type="var">A</span>) (<span class="id" type="var">n</span> : <span class="id" type="var">nat</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">n</span> = <span class="id" type="var">length</span> <span class="id" type="var">l</span> → <span class="id" type="var">nth</span> <span class="id" type="var">n</span> (<span class="id" type="var">l</span> ++ <span class="id" type="var">x</span>::<span class="id" type="var">nil</span>) <span class="id" type="var">d</span> = <span class="id" type="var">x</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">intros</span>. <span class="id" type="tactic">subst</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">nth_eq_last</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
The proof case for <span class="inlinecode"><span class="id" type="var">ref</span></span> from the preservation theorem then
    becomes much easier to prove, because <span class="inlinecode"><span class="id" type="tactic">rewrite</span></span> <span class="inlinecode"><span class="id" type="var">nth_eq_last'</span></span>
    now succeeds. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">preservation_ref</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">st</span>:<span class="id" type="var">store</span>) (<span class="id" type="var">ST</span> : <span class="id" type="var">store_ty</span>) <span class="id" type="var">T<sub>1</sub></span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">length</span> <span class="id" type="var">ST</span> = <span class="id" type="var">length</span> <span class="id" type="var">st</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">Ref</span> <span class="id" type="var">T<sub>1</sub></span> = <span class="id" type="var">Ref</span> (<span class="id" type="var">store_Tlookup</span> (<span class="id" type="var">length</span> <span class="id" type="var">st</span>) (<span class="id" type="var">ST</span> ++ <span class="id" type="var">T<sub>1</sub></span>::<span class="id" type="var">nil</span>)).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span>. <span class="id" type="var">dup</span>.<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;A&nbsp;first&nbsp;proof,&nbsp;with&nbsp;an&nbsp;explicit&nbsp;<span class="inlinecode"><span class="id" type="tactic">unfold</span></span>&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">store_Tlookup</span>. <span class="id" type="tactic">rewrite</span>* <span class="id" type="var">nth_eq_last'</span>.<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;A&nbsp;second&nbsp;proof,&nbsp;with&nbsp;a&nbsp;call&nbsp;to&nbsp;<span class="inlinecode"><span class="id" type="var">fequal</span></span>&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="var">fequal</span>. <span class="id" type="tactic">symmetry</span>. <span class="id" type="tactic">apply</span>* <span class="id" type="var">nth_eq_last'</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
The optimized proof of preservation is summarized next. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">preservation'</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">ST</span> <span class="id" type="var">t</span> <span class="id" type="var">t'</span> <span class="id" type="var">T</span> <span class="id" type="var">st</span> <span class="id" type="var">st'</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">has_type</span> <span class="id" type="var">empty</span> <span class="id" type="var">ST</span> <span class="id" type="var">t</span> <span class="id" type="var">T</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">store_well_typed</span> <span class="id" type="var">ST</span> <span class="id" type="var">st</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">t</span> / <span class="id" type="var">st</span> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> <span class="id" type="var">t'</span> / <span class="id" type="var">st'</span> →<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">ST'</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">extends</span> <span class="id" type="var">ST'</span> <span class="id" type="var">ST</span> ∧<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">has_type</span> <span class="id" type="var">empty</span> <span class="id" type="var">ST'</span> <span class="id" type="var">t'</span> <span class="id" type="var">T</span> ∧<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">store_well_typed</span> <span class="id" type="var">ST'</span> <span class="id" type="var">st'</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">remember</span> (@<span class="id" type="var">empty</span> <span class="id" type="var">ty</span>) <span class="id" type="keyword">as</span> <span class="id" type="var">Gamma</span>. <span class="id" type="var">introv</span> <span class="id" type="var">Ht</span>. <span class="id" type="var">gen</span> <span class="id" type="var">t'</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">Ht</span>; <span class="id" type="var">introv</span> <span class="id" type="var">HST</span> <span class="id" type="var">Hstep</span>; <span class="id" type="tactic">subst</span> <span class="id" type="var">Gamma</span>; <span class="id" type="var">inverts</span> <span class="id" type="var">Hstep</span>; <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;- <span style='font-size:120%;'>&exist;</span><span class="id" type="var">ST</span>. <span class="id" type="var">inverts</span> <span class="id" type="var">Ht<sub>1</sub></span>. <span class="id" type="var">splits</span>*. <span class="id" type="var">applys</span>* <span class="id" type="var">substitution_preserves_typing</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="var">forwards</span>*: <span class="id" type="var">IHHt1</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="var">forwards</span>*: <span class="id" type="var">IHHt2</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="var">forwards</span>*: <span class="id" type="var">IHHt</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="var">forwards</span>*: <span class="id" type="var">IHHt</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="var">forwards</span>*: <span class="id" type="var">IHHt1</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="var">forwards</span>*: <span class="id" type="var">IHHt2</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="var">forwards</span>*: <span class="id" type="var">IHHt1</span>.<br/>
&nbsp;&nbsp;- <span style='font-size:120%;'>&exist;</span>(<span class="id" type="var">ST</span> ++ <span class="id" type="var">T<sub>1</sub></span>::<span class="id" type="var">nil</span>). <span class="id" type="var">inverts</span> <span class="id" type="var">keep</span> <span class="id" type="var">HST</span>. <span class="id" type="var">splits</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">extends_app</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">applys_eq</span> <span class="id" type="var">T_Loc</span> 1.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">app_length</span>. <span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">omega</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">store_Tlookup</span>. <span class="id" type="tactic">rewrite</span>* <span class="id" type="var">nth_eq_last'</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span>* <span class="id" type="var">store_well_typed_app</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="var">forwards</span>*: <span class="id" type="var">IHHt</span>.<br/>
&nbsp;&nbsp;- <span style='font-size:120%;'>&exist;</span><span class="id" type="var">ST</span>. <span class="id" type="var">splits</span>*. <span class="id" type="var">lets</span> [<span class="id" type="var">_</span> <span class="id" type="var">Hsty</span>]: <span class="id" type="var">HST</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">applys_eq</span>* <span class="id" type="var">Hsty</span> 1. <span class="id" type="var">inverts</span>* <span class="id" type="var">Ht</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="var">forwards</span>*: <span class="id" type="var">IHHt</span>.<br/>
&nbsp;&nbsp;- <span style='font-size:120%;'>&exist;</span><span class="id" type="var">ST</span>. <span class="id" type="var">splits</span>*. <span class="id" type="var">applys</span>* <span class="id" type="var">assign_pres_store_typing</span>. <span class="id" type="var">inverts</span>* <span class="id" type="var">Ht<sub>1</sub></span>.<br/>
&nbsp;&nbsp;- <span class="id" type="var">forwards</span>*: <span class="id" type="var">IHHt1</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="var">forwards</span>*: <span class="id" type="var">IHHt2</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab564"></a><h2 class="section">Progress for STLCRef</h2>

<div class="paragraph"> </div>

 The proof of progress for <span class="inlinecode"><span class="id" type="var">STLCRef</span></span> can be found in chapter
    <span class="inlinecode"><span class="id" type="var">References</span></span>. The optimized proof script is, here again, about
    half the length. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="tactic">progress</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">ST</span> <span class="id" type="var">t</span> <span class="id" type="var">T</span> <span class="id" type="var">st</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">has_type</span> <span class="id" type="var">empty</span> <span class="id" type="var">ST</span> <span class="id" type="var">t</span> <span class="id" type="var">T</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">store_well_typed</span> <span class="id" type="var">ST</span> <span class="id" type="var">st</span> →<br/>
&nbsp;&nbsp;(<span class="id" type="var">value</span> <span class="id" type="var">t</span> ∨ <span style='font-size:120%;'>&exist;</span><span class="id" type="var">t'</span> <span class="id" type="var">st'</span>, <span class="id" type="var">t</span> / <span class="id" type="var">st</span> <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> <span class="id" type="var">t'</span> / <span class="id" type="var">st'</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">introv</span> <span class="id" type="var">Ht</span> <span class="id" type="var">HST</span>. <span class="id" type="var">remember</span> (@<span class="id" type="var">empty</span> <span class="id" type="var">ty</span>) <span class="id" type="keyword">as</span> <span class="id" type="var">Gamma</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">Ht</span>; <span class="id" type="tactic">subst</span> <span class="id" type="var">Gamma</span>; <span class="id" type="var">tryfalse</span>; <span class="id" type="tactic">try</span> <span class="id" type="var">solve</span> [<span class="id" type="var">left</span>*].<br/>
&nbsp;&nbsp;- <span class="id" type="var">right</span>. <span class="id" type="tactic">destruct</span>* <span class="id" type="var">IHHt1</span> <span class="id" type="keyword">as</span> [<span class="id" type="var">K</span>|].<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">inverts</span> <span class="id" type="var">K</span>; <span class="id" type="var">inverts</span> <span class="id" type="var">Ht<sub>1</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span>* <span class="id" type="var">IHHt2</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="var">right</span>. <span class="id" type="tactic">destruct</span>* <span class="id" type="var">IHHt</span> <span class="id" type="keyword">as</span> [<span class="id" type="var">K</span>|].<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">inverts</span> <span class="id" type="var">K</span>; <span class="id" type="tactic">try</span> <span class="id" type="var">solve</span> [<span class="id" type="var">inverts</span> <span class="id" type="var">Ht</span>]. <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="var">right</span>. <span class="id" type="tactic">destruct</span>* <span class="id" type="var">IHHt</span> <span class="id" type="keyword">as</span> [<span class="id" type="var">K</span>|].<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">inverts</span> <span class="id" type="var">K</span>; <span class="id" type="tactic">try</span> <span class="id" type="var">solve</span> [<span class="id" type="var">inverts</span> <span class="id" type="var">Ht</span>]. <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="var">right</span>. <span class="id" type="tactic">destruct</span>* <span class="id" type="var">IHHt1</span> <span class="id" type="keyword">as</span> [<span class="id" type="var">K</span>|].<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">inverts</span> <span class="id" type="var">K</span>; <span class="id" type="tactic">try</span> <span class="id" type="var">solve</span> [<span class="id" type="var">inverts</span> <span class="id" type="var">Ht<sub>1</sub></span>].<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span>* <span class="id" type="var">IHHt2</span> <span class="id" type="keyword">as</span> [<span class="id" type="var">M</span>|].<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">inverts</span> <span class="id" type="var">M</span>; <span class="id" type="tactic">try</span> <span class="id" type="var">solve</span> [<span class="id" type="var">inverts</span> <span class="id" type="var">Ht<sub>2</sub></span>]. <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="var">right</span>. <span class="id" type="tactic">destruct</span>* <span class="id" type="var">IHHt1</span> <span class="id" type="keyword">as</span> [<span class="id" type="var">K</span>|].<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">inverts</span> <span class="id" type="var">K</span>; <span class="id" type="tactic">try</span> <span class="id" type="var">solve</span> [<span class="id" type="var">inverts</span> <span class="id" type="var">Ht<sub>1</sub></span>]. <span class="id" type="tactic">destruct</span>* <span class="id" type="var">n</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="var">right</span>. <span class="id" type="tactic">destruct</span>* <span class="id" type="var">IHHt</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="var">right</span>. <span class="id" type="tactic">destruct</span>* <span class="id" type="var">IHHt</span> <span class="id" type="keyword">as</span> [<span class="id" type="var">K</span>|].<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">inverts</span> <span class="id" type="var">K</span>; <span class="id" type="var">inverts</span> <span class="id" type="var">Ht</span> <span class="id" type="keyword">as</span> <span class="id" type="var">M</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">inverts</span> <span class="id" type="var">HST</span> <span class="id" type="keyword">as</span> <span class="id" type="var">N</span>. <span class="id" type="tactic">rewrite</span>* <span class="id" type="var">N</span> <span class="id" type="keyword">in</span> <span class="id" type="var">M</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="var">right</span>. <span class="id" type="tactic">destruct</span>* <span class="id" type="var">IHHt1</span> <span class="id" type="keyword">as</span> [<span class="id" type="var">K</span>|].<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span>* <span class="id" type="var">IHHt2</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">inverts</span> <span class="id" type="var">K</span>; <span class="id" type="var">inverts</span> <span class="id" type="var">Ht<sub>1</sub></span> <span class="id" type="keyword">as</span> <span class="id" type="var">M</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">inverts</span> <span class="id" type="var">HST</span> <span class="id" type="keyword">as</span> <span class="id" type="var">N</span>. <span class="id" type="tactic">rewrite</span>* <span class="id" type="var">N</span> <span class="id" type="keyword">in</span> <span class="id" type="var">M</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">End</span> <span class="id" type="var">PreservationProgressReferences</span>.<br/>
</div>

<div class="doc">
<a name="lab565"></a><h2 class="section">Subtyping</h2>

</div>
<div class="code code-space">

<br/>
<span class="id" type="var">From</span> <span class="id" type="var">PLF</span> <span class="id" type="keyword">Require</span> <span class="id" type="var">Sub</span>.<br/>
<span class="id" type="keyword">Module</span> <span class="id" type="var">SubtypingInversion</span>.<br/>
<span class="id" type="keyword">Import</span> <span class="id" type="var">Sub</span>.<br/>
</div>

<div class="doc">
Consider the inversion lemma for typing judgment
    of abstractions in a type system with subtyping. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">abs_arrow</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">x</span> <span class="id" type="var">S<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub></span> <span class="id" type="var">T<sub>1</sub></span> <span class="id" type="var">T<sub>2</sub></span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">has_type</span> <span class="id" type="var">empty</span> (<span class="id" type="var">abs</span> <span class="id" type="var">x</span> <span class="id" type="var">S<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub></span>) (<span class="id" type="var">Arrow</span> <span class="id" type="var">T<sub>1</sub></span> <span class="id" type="var">T<sub>2</sub></span>) →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">subtype</span> <span class="id" type="var">T<sub>1</sub></span> <span class="id" type="var">S<sub>1</sub></span><br/>
&nbsp;&nbsp;∧ <span class="id" type="var">has_type</span> (<span class="id" type="var">update</span> <span class="id" type="var">empty</span> <span class="id" type="var">x</span> <span class="id" type="var">S<sub>1</sub></span>) <span class="id" type="var">s<sub>2</sub></span> <span class="id" type="var">T<sub>2</sub></span>.<br/>
<span class="id" type="keyword">Proof</span> <span class="id" type="keyword">with</span> <span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">x</span> <span class="id" type="var">S<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub></span> <span class="id" type="var">T<sub>1</sub></span> <span class="id" type="var">T<sub>2</sub></span> <span class="id" type="var">Hty</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">typing_inversion_abs</span> <span class="id" type="keyword">in</span> <span class="id" type="var">Hty</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">Hty</span> <span class="id" type="keyword">as</span> [<span class="id" type="var">S<sub>2</sub></span> [<span class="id" type="var">Hsub</span> <span class="id" type="var">Hty</span>]].<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">sub_inversion_arrow</span> <span class="id" type="keyword">in</span> <span class="id" type="var">Hsub</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">Hsub</span> <span class="id" type="keyword">as</span> [<span class="id" type="var">U<sub>1</sub></span> [<span class="id" type="var">U<sub>2</sub></span> [<span class="id" type="var">Heq</span> [<span class="id" type="var">Hsub1</span> <span class="id" type="var">Hsub2</span>]]]].<br/>
&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">Heq</span>; <span class="id" type="tactic">subst</span>...<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
Exercise: optimize the proof script, using
    <span class="inlinecode"><span class="id" type="var">introv</span></span>, <span class="inlinecode"><span class="id" type="var">lets</span></span> and <span class="inlinecode"><span class="id" type="var">inverts</span>*</span>. In particular,
    you will find it useful to replace the pattern
    <span class="inlinecode"><span class="id" type="tactic">apply</span></span> <span class="inlinecode"><span class="id" type="var">K</span></span> <span class="inlinecode"><span class="id" type="keyword">in</span></span> <span class="inlinecode"><span class="id" type="var">H</span>.</span> <span class="inlinecode"><span class="id" type="tactic">destruct</span></span> <span class="inlinecode"><span class="id" type="var">H</span></span> <span class="inlinecode"><span class="id" type="keyword">as</span></span> <span class="inlinecode"><span class="id" type="var">I</span></span> with <span class="inlinecode"><span class="id" type="var">lets</span></span> <span class="inlinecode"><span class="id" type="var">I</span>:</span> <span class="inlinecode"><span class="id" type="var">K</span></span> <span class="inlinecode"><span class="id" type="var">H</span></span>.
    The solution fits on 3 lines. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">abs_arrow'</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">x</span> <span class="id" type="var">S<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub></span> <span class="id" type="var">T<sub>1</sub></span> <span class="id" type="var">T<sub>2</sub></span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">has_type</span> <span class="id" type="var">empty</span> (<span class="id" type="var">abs</span> <span class="id" type="var">x</span> <span class="id" type="var">S<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub></span>) (<span class="id" type="var">Arrow</span> <span class="id" type="var">T<sub>1</sub></span> <span class="id" type="var">T<sub>2</sub></span>) →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">subtype</span> <span class="id" type="var">T<sub>1</sub></span> <span class="id" type="var">S<sub>1</sub></span><br/>
&nbsp;&nbsp;∧ <span class="id" type="var">has_type</span> (<span class="id" type="var">update</span> <span class="id" type="var">empty</span> <span class="id" type="var">x</span> <span class="id" type="var">S<sub>1</sub></span>) <span class="id" type="var">s<sub>2</sub></span> <span class="id" type="var">T<sub>2</sub></span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">admit</span>.<br/>
<span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">End</span> <span class="id" type="var">SubtypingInversion</span>.<br/>
</div>

<div class="doc">
<a name="lab566"></a><h1 class="section">Advanced Topics in Proof Search</h1>

</div>
<div class="code code-space">

<br/>
</div>

<div class="doc">
<a name="lab567"></a><h2 class="section">Stating Lemmas in the Right Way</h2>

<div class="paragraph"> </div>

 Due to its depth-first strategy, <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> can get exponentially
    slower as the depth search increases, even when a short proof
    exists. In general, to make proof search run reasonably fast, one
    should avoid using a depth search greater than 5 or 6. Moreover,
    one should try to minimize the number of applicable lemmas, and
    usually put first the hypotheses whose proof usefully instantiates
    the existential variables.

<div class="paragraph"> </div>

    In fact, the ability for <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> to solve certain goals actually
    depends on the order in which the hypotheses are stated. This point
    is illustrated through the following example, in which <span class="inlinecode"><span class="id" type="var">P</span></span> is
    a property of natural numbers. This property is such that
    <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> holds for any <span class="inlinecode"><span class="id" type="var">n</span></span> as soon as <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">m</span></span> holds for at least one <span class="inlinecode"><span class="id" type="var">m</span></span>
    different from zero. The goal is to prove that <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">2</span> implies <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">1</span>.
    When the hypothesis about <span class="inlinecode"><span class="id" type="var">P</span></span> is stated in the form
    <span class="inlinecode"><span style='font-size:120%;'>&forall;</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode"><span class="id" type="var">m</span>,</span> <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">m</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">m</span></span> <span class="inlinecode">≠</span> <span class="inlinecode">0</span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span>, then <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> works. However, with
    <span class="inlinecode"><span style='font-size:120%;'>&forall;</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode"><span class="id" type="var">m</span>,</span> <span class="inlinecode"><span class="id" type="var">m</span></span> <span class="inlinecode">≠</span> <span class="inlinecode">0</span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">m</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span>, the tactic <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> fails. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">order_matters_1</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">P</span> : <span class="id" type="var">nat</span>→<span class="id" type="keyword">Prop</span>),<br/>
&nbsp;&nbsp;(<span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span> <span class="id" type="var">m</span>, <span class="id" type="var">P</span> <span class="id" type="var">m</span> → <span class="id" type="var">m</span> ≠ 0 → <span class="id" type="var">P</span> <span class="id" type="var">n</span>) →<br/>
&nbsp;&nbsp;<span class="id" type="var">P</span> 2 →<br/>
&nbsp;&nbsp;<span class="id" type="var">P</span> 1.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">eauto</span>. <span class="comment">(*&nbsp;Success&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;The&nbsp;proof:&nbsp;<span class="inlinecode"><span class="id" type="tactic">intros</span></span> <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">H</span></span> <span class="inlinecode"><span class="id" type="var">K</span>.</span> <span class="inlinecode"><span class="id" type="tactic">eapply</span></span> <span class="inlinecode"><span class="id" type="var">H</span>.</span> <span class="inlinecode"><span class="id" type="tactic">apply</span></span> <span class="inlinecode"><span class="id" type="var">K</span>.</span> <span class="inlinecode"><span class="id" type="tactic">auto</span>.</span>&nbsp;*)</span><br/>
<span class="id" type="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">order_matters_2</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">P</span> : <span class="id" type="var">nat</span>→<span class="id" type="keyword">Prop</span>),<br/>
&nbsp;&nbsp;(<span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span> <span class="id" type="var">m</span>, <span class="id" type="var">m</span> ≠ 0 → <span class="id" type="var">P</span> <span class="id" type="var">m</span> → <span class="id" type="var">P</span> <span class="id" type="var">n</span>) →<br/>
&nbsp;&nbsp;<span class="id" type="var">P</span> 5 →<br/>
&nbsp;&nbsp;<span class="id" type="var">P</span> 1.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">eauto</span>. <span class="comment">(*&nbsp;Failure&nbsp;*)</span><br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;To&nbsp;understand&nbsp;why,&nbsp;let&nbsp;us&nbsp;replay&nbsp;the&nbsp;previous&nbsp;proof&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">P</span> <span class="id" type="var">H</span> <span class="id" type="var">K</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">eapply</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;The&nbsp;application&nbsp;of&nbsp;<span class="inlinecode"><span class="id" type="tactic">eapply</span></span>&nbsp;has&nbsp;left&nbsp;two&nbsp;subgoals,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode">?<span class="id" type="var">X</span></span> <span class="inlinecode">≠</span> <span class="inlinecode">0</span>&nbsp;and&nbsp;<span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">?<span class="id" type="var">X</span></span>,&nbsp;where&nbsp;<span class="inlinecode">?<span class="id" type="var">X</span></span>&nbsp;is&nbsp;an&nbsp;existential&nbsp;variable.&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;Solving&nbsp;the&nbsp;first&nbsp;subgoal&nbsp;is&nbsp;easy&nbsp;for&nbsp;<span class="inlinecode"><span class="id" type="tactic">eauto</span></span>:&nbsp;it&nbsp;suffices<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;to&nbsp;instantiate&nbsp;<span class="inlinecode">?<span class="id" type="var">X</span></span>&nbsp;as&nbsp;the&nbsp;value&nbsp;<span class="inlinecode">1</span>,&nbsp;which&nbsp;is&nbsp;the&nbsp;simplest<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;value&nbsp;that&nbsp;satisfies&nbsp;<span class="inlinecode">?<span class="id" type="var">X</span></span> <span class="inlinecode">≠</span> <span class="inlinecode">0</span>.&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;But&nbsp;then&nbsp;the&nbsp;second&nbsp;goal&nbsp;becomes&nbsp;<span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">1</span>,&nbsp;which&nbsp;is&nbsp;where&nbsp;we<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;started&nbsp;from.&nbsp;So,&nbsp;<span class="inlinecode"><span class="id" type="tactic">eauto</span></span>&nbsp;gets&nbsp;stuck&nbsp;at&nbsp;this&nbsp;point.&nbsp;*)</span><br/>
<span class="id" type="keyword">Abort</span>.<br/>
</div>

<div class="doc">
It is very important to understand that the hypothesis <span class="inlinecode"><span style='font-size:120%;'>&forall;</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span>
    <span class="inlinecode"><span class="id" type="var">m</span>,</span> <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">m</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">m</span></span> <span class="inlinecode">≠</span> <span class="inlinecode">0</span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> is eauto-friendly, whereas <span class="inlinecode"><span style='font-size:120%;'>&forall;</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode"><span class="id" type="var">m</span>,</span> <span class="inlinecode"><span class="id" type="var">m</span></span>
    <span class="inlinecode">≠</span> <span class="inlinecode">0</span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">m</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> really isn't.  Guessing a value of <span class="inlinecode"><span class="id" type="var">m</span></span> for
    which <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">m</span></span> holds and then checking that <span class="inlinecode"><span class="id" type="var">m</span></span> <span class="inlinecode">≠</span> <span class="inlinecode">0</span> holds works well
    because there are few values of <span class="inlinecode"><span class="id" type="var">m</span></span> for which <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">m</span></span> holds. So, it
    is likely that <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> comes up with the right one. On the other
    hand, guessing a value of <span class="inlinecode"><span class="id" type="var">m</span></span> for which <span class="inlinecode"><span class="id" type="var">m</span></span> <span class="inlinecode">≠</span> <span class="inlinecode">0</span> and then checking
    that <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">m</span></span> holds does not work well, because there are many values
    of <span class="inlinecode"><span class="id" type="var">m</span></span> that satisfy <span class="inlinecode"><span class="id" type="var">m</span></span> <span class="inlinecode">≠</span> <span class="inlinecode">0</span> but not <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">m</span></span>. 
</div>

<div class="doc">
<a name="lab568"></a><h2 class="section">Unfolding of Definitions During Proof-Search</h2>

<div class="paragraph"> </div>

 The use of intermediate definitions is generally encouraged in a
    formal development as it usually leads to more concise and more
    readable statements. Yet, definitions can make it a little harder
    to automate proofs. The problem is that it is not obvious for a
    proof search mechanism to know when definitions need to be
    unfolded. Note that a naive strategy that consists in unfolding
    all definitions before calling proof search does not scale up to
    large proofs, so we avoid it. This section introduces a few
    techniques for avoiding to manually unfold definitions before
    calling proof search. 
<div class="paragraph"> </div>

 To illustrate the treatment of definitions, let <span class="inlinecode"><span class="id" type="var">P</span></span> be an abstract
    property on natural numbers, and let <span class="inlinecode"><span class="id" type="var">myFact</span></span> be a definition
    denoting the proposition <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span> holds for any <span class="inlinecode"><span class="id" type="var">x</span></span> less than or
    equal to 3. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Axiom</span> <span class="id" type="var">P</span> : <span class="id" type="var">nat</span> → <span class="id" type="keyword">Prop</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">myFact</span> := <span style='font-size:120%;'>&forall;</span><span class="id" type="var">x</span>, <span class="id" type="var">x</span> ≤ 3 → <span class="id" type="var">P</span> <span class="id" type="var">x</span>.<br/>
</div>

<div class="doc">
Proving that <span class="inlinecode"><span class="id" type="var">myFact</span></span> under the assumption that <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span> holds for
    any <span class="inlinecode"><span class="id" type="var">x</span></span> should be trivial. Yet, <span class="inlinecode"><span class="id" type="tactic">auto</span></span> fails to prove it unless we
    unfold the definition of <span class="inlinecode"><span class="id" type="var">myFact</span></span> explicitly. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">demo_hint_unfold_goal_1</span> :<br/>
&nbsp;&nbsp;(<span style='font-size:120%;'>&forall;</span><span class="id" type="var">x</span>, <span class="id" type="var">P</span> <span class="id" type="var">x</span>) →<br/>
&nbsp;&nbsp;<span class="id" type="var">myFact</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">auto</span>. <span class="comment">(*&nbsp;Proof&nbsp;search&nbsp;doesn't&nbsp;know&nbsp;what&nbsp;to&nbsp;do,&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">myFact</span>. <span class="id" type="tactic">auto</span>. <span class="comment">(*&nbsp;unless&nbsp;we&nbsp;unfold&nbsp;the&nbsp;definition.&nbsp;*)</span><br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
To automate the unfolding of definitions that appear as proof
    obligation, one can use the command <span class="inlinecode"><span class="id" type="keyword">Hint</span></span> <span class="inlinecode"><span class="id" type="keyword">Unfold</span></span> <span class="inlinecode"><span class="id" type="var">myFact</span></span> to tell
    Coq that it should always try to unfold <span class="inlinecode"><span class="id" type="var">myFact</span></span> when <span class="inlinecode"><span class="id" type="var">myFact</span></span>
    appears in the goal. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Hint</span> <span class="id" type="keyword">Unfold</span> <span class="id" type="var">myFact</span>.<br/>
</div>

<div class="doc">
This time, automation is able to see through the definition
    of <span class="inlinecode"><span class="id" type="var">myFact</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">demo_hint_unfold_goal_2</span> :<br/>
&nbsp;&nbsp;(<span style='font-size:120%;'>&forall;</span><span class="id" type="var">x</span>, <span class="id" type="var">P</span> <span class="id" type="var">x</span>) →<br/>
&nbsp;&nbsp;<span class="id" type="var">myFact</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">auto</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
However, the <span class="inlinecode"><span class="id" type="keyword">Hint</span></span> <span class="inlinecode"><span class="id" type="keyword">Unfold</span></span> mechanism only works for unfolding
    definitions that appear in the goal. In general, proof search does
    not unfold definitions from the context. For example, assume we
    want to prove that <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">3</span> holds under the assumption that <span class="inlinecode"><span class="id" type="var">True</span></span> <span class="inlinecode">→</span>
    <span class="inlinecode"><span class="id" type="var">myFact</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">demo_hint_unfold_context_1</span> :<br/>
&nbsp;&nbsp;(<span class="id" type="var">True</span> → <span class="id" type="var">myFact</span>) →<br/>
&nbsp;&nbsp;<span class="id" type="var">P</span> 3.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">auto</span>. <span class="comment">(*&nbsp;fails&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">myFact</span> <span class="id" type="keyword">in</span> *. <span class="id" type="tactic">auto</span>. <span class="comment">(*&nbsp;succeeds&nbsp;*)</span><br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
There is actually one exception to the previous rule: a constant
    occuring in an hypothesis is automatically unfolded if the
    hypothesis can be directly applied to the current goal. For example,
    <span class="inlinecode"><span class="id" type="tactic">auto</span></span> can prove <span class="inlinecode"><span class="id" type="var">myFact</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">3</span>, as illustrated below. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">demo_hint_unfold_context_2</span> :<br/>
&nbsp;&nbsp;<span class="id" type="var">myFact</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">P</span> 3.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">auto</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab569"></a><h2 class="section">Automation for Proving Absurd Goals</h2>

<div class="paragraph"> </div>

 In this section, we'll see that lemmas concluding on a negation
    are generally not useful as hints, and that lemmas whose
    conclusion is <span class="inlinecode"><span class="id" type="var">False</span></span> can be useful hints but having too many of
    them makes proof search inefficient. We'll also see a practical
    work-around to the efficiency issue. 
<div class="paragraph"> </div>

 Consider the following lemma, which asserts that a number
    less than or equal to 3 is not greater than 3. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Parameter</span> <span class="id" type="var">le_not_gt</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">x</span>,<br/>
&nbsp;&nbsp;(<span class="id" type="var">x</span> ≤ 3) →<br/>
&nbsp;&nbsp;¬(<span class="id" type="var">x</span> &gt; 3).<br/>
</div>

<div class="doc">
Equivalently, one could state that a number greater than three is
    not less than or equal to 3. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Parameter</span> <span class="id" type="var">gt_not_le</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">x</span>,<br/>
&nbsp;&nbsp;(<span class="id" type="var">x</span> &gt; 3) →<br/>
&nbsp;&nbsp;¬(<span class="id" type="var">x</span> ≤ 3).<br/>
</div>

<div class="doc">
In fact, both statements are equivalent to a third one stating
    that <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode">≤</span> <span class="inlinecode">3</span> and <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode">&gt;</span> <span class="inlinecode">3</span> are contradictory, in the sense that
    they imply <span class="inlinecode"><span class="id" type="var">False</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Parameter</span> <span class="id" type="var">le_gt_false</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">x</span>,<br/>
&nbsp;&nbsp;(<span class="id" type="var">x</span> ≤ 3) →<br/>
&nbsp;&nbsp;(<span class="id" type="var">x</span> &gt; 3) →<br/>
&nbsp;&nbsp;<span class="id" type="var">False</span>.<br/>
</div>

<div class="doc">
The following investigation aim at figuring out which of the three
    statments is the most convenient with respect to proof
    automation. The following material is enclosed inside a <span class="inlinecode"><span class="id" type="keyword">Section</span></span>,
    so as to restrict the scope of the hints that we are adding. In
    other words, after the end of the section, the hints added within
    the section will no longer be active. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Section</span> <span class="id" type="var">DemoAbsurd1</span>.<br/>
</div>

<div class="doc">
Let's try to add the first lemma, <span class="inlinecode"><span class="id" type="var">le_not_gt</span></span>, as hint,
    and see whether we can prove that the proposition
    <span class="inlinecode"><span style='font-size:120%;'>&exist;</span></span> <span class="inlinecode"><span class="id" type="var">x</span>,</span> <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode">≤</span> <span class="inlinecode">3</span> <span class="inlinecode">∧</span> <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode">&gt;</span> <span class="inlinecode">3</span> is absurd. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Hint</span> <span class="id" type="keyword">Resolve</span> <span class="id" type="var">le_not_gt</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">demo_auto_absurd_1</span> :<br/>
&nbsp;&nbsp;(<span style='font-size:120%;'>&exist;</span><span class="id" type="var">x</span>, <span class="id" type="var">x</span> ≤ 3 ∧ <span class="id" type="var">x</span> &gt; 3) →<br/>
&nbsp;&nbsp;<span class="id" type="var">False</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span>. <span class="id" type="var">jauto_set</span>. <span class="comment">(*&nbsp;decomposes&nbsp;the&nbsp;assumption&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;debug&nbsp;*)</span> <span class="id" type="tactic">eauto</span>. <span class="comment">(*&nbsp;does&nbsp;not&nbsp;see&nbsp;that&nbsp;<span class="inlinecode"><span class="id" type="var">le_not_gt</span></span>&nbsp;could&nbsp;apply&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="tactic">eapply</span> <span class="id" type="var">le_not_gt</span>. <span class="id" type="tactic">eauto</span>. <span class="id" type="tactic">eauto</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
The lemma <span class="inlinecode"><span class="id" type="var">gt_not_le</span></span> is symmetric to <span class="inlinecode"><span class="id" type="var">le_not_gt</span></span>, so it will not
    be any better. The third lemma, <span class="inlinecode"><span class="id" type="var">le_gt_false</span></span>, is a more useful
    hint, because it concludes on <span class="inlinecode"><span class="id" type="var">False</span></span>, so proof search will try to
    apply it when the current goal is <span class="inlinecode"><span class="id" type="var">False</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Hint</span> <span class="id" type="keyword">Resolve</span> <span class="id" type="var">le_gt_false</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">demo_auto_absurd_2</span> :<br/>
&nbsp;&nbsp;(<span style='font-size:120%;'>&exist;</span><span class="id" type="var">x</span>, <span class="id" type="var">x</span> ≤ 3 ∧ <span class="id" type="var">x</span> &gt; 3) →<br/>
&nbsp;&nbsp;<span class="id" type="var">False</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">dup</span>.<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;detailed&nbsp;version:&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span>. <span class="id" type="var">jauto_set</span>. <span class="comment">(*&nbsp;debug&nbsp;*)</span> <span class="id" type="tactic">eauto</span>.<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;short&nbsp;version:&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="var">jauto</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
In summary, a lemma of the form <span class="inlinecode"><span class="id" type="var">H<sub>1</sub></span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">H<sub>2</sub></span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">False</span></span> is a much more
    effective hint than <span class="inlinecode"><span class="id" type="var">H<sub>1</sub></span></span> <span class="inlinecode">→</span> <span class="inlinecode">¬</span> <span class="inlinecode"><span class="id" type="var">H<sub>2</sub></span></span>, even though the two statments
    are equivalent up to the definition of the negation symbol <span class="inlinecode">¬</span>. 
<div class="paragraph"> </div>

 That said, one should be careful with adding lemmas whose
    conclusion is <span class="inlinecode"><span class="id" type="var">False</span></span> as hint. The reason is that whenever
    reaching the goal <span class="inlinecode"><span class="id" type="var">False</span></span>, the proof search mechanism will
    potentially try to apply all the hints whose conclusion is <span class="inlinecode"><span class="id" type="var">False</span></span>
    before applying the appropriate one.  
</div>
<div class="code code-tight">

<span class="id" type="keyword">End</span> <span class="id" type="var">DemoAbsurd1</span>.<br/>
</div>

<div class="doc">
Adding lemmas whose conclusion is <span class="inlinecode"><span class="id" type="var">False</span></span> as hint can be, locally,
    a very effective solution. However, this approach does not scale
    up for global hints.  For most practical applications, it is
    reasonable to give the name of the lemmas to be exploited for
    deriving a contradiction. The tactic <span class="inlinecode"><span class="id" type="var">false</span></span> <span class="inlinecode"><span class="id" type="var">H</span></span>, provided by
    <span class="inlinecode"><span class="id" type="var">LibTactics</span></span> serves that purpose: <span class="inlinecode"><span class="id" type="var">false</span></span> <span class="inlinecode"><span class="id" type="var">H</span></span> replaces the goal
    with <span class="inlinecode"><span class="id" type="var">False</span></span> and calls <span class="inlinecode"><span class="id" type="tactic">eapply</span></span> <span class="inlinecode"><span class="id" type="var">H</span></span>. Its behavior is described next.
    Observe that any of the three statements <span class="inlinecode"><span class="id" type="var">le_not_gt</span></span>, <span class="inlinecode"><span class="id" type="var">gt_not_le</span></span>
    or <span class="inlinecode"><span class="id" type="var">le_gt_false</span></span> can be used. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">demo_false</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">x</span>,<br/>
&nbsp;&nbsp;(<span class="id" type="var">x</span> ≤ 3) →<br/>
&nbsp;&nbsp;(<span class="id" type="var">x</span> &gt; 3) →<br/>
&nbsp;&nbsp;4 = 5.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span>. <span class="id" type="var">dup</span> 4.<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;A&nbsp;failed&nbsp;proof:&nbsp;*)</span><br/>
&nbsp;&nbsp;- <span class="id" type="var">false</span>. <span class="id" type="tactic">eapply</span> <span class="id" type="var">le_gt_false</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="id" type="tactic">auto</span>. <span class="comment">(*&nbsp;here,&nbsp;<span class="inlinecode"><span class="id" type="tactic">auto</span></span>&nbsp;does&nbsp;not&nbsp;prove&nbsp;<span class="inlinecode">?<span class="id" type="var">x</span></span> <span class="inlinecode">≤</span> <span class="inlinecode">3</span>&nbsp;by&nbsp;using&nbsp;<span class="inlinecode"><span class="id" type="var">H</span></span>&nbsp;but<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;by&nbsp;using&nbsp;the&nbsp;lemma&nbsp;<span class="inlinecode"><span class="id" type="var">le_refl</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span style='font-size:120%;'>&forall;</span></span> <span class="inlinecode"><span class="id" type="var">x</span>,</span> <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode">≤</span> <span class="inlinecode"><span class="id" type="var">x</span></span>.&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;The&nbsp;second&nbsp;subgoal&nbsp;becomes&nbsp;<span class="inlinecode">3</span> <span class="inlinecode">&gt;</span> <span class="inlinecode">3</span>,&nbsp;which&nbsp;is&nbsp;not&nbsp;provable.&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="id" type="var">skip</span>.<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;A&nbsp;correct&nbsp;proof:&nbsp;*)</span><br/>
&nbsp;&nbsp;- <span class="id" type="var">false</span>. <span class="id" type="tactic">eapply</span> <span class="id" type="var">le_gt_false</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="id" type="tactic">eauto</span>. <span class="comment">(*&nbsp;here,&nbsp;<span class="inlinecode"><span class="id" type="tactic">eauto</span></span>&nbsp;uses&nbsp;<span class="inlinecode"><span class="id" type="var">H</span></span>,&nbsp;as&nbsp;expected,&nbsp;to&nbsp;prove&nbsp;<span class="inlinecode">?<span class="id" type="var">x</span></span> <span class="inlinecode">≤</span> <span class="inlinecode">3</span>&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="id" type="tactic">eauto</span>. <span class="comment">(*&nbsp;so&nbsp;the&nbsp;second&nbsp;subgoal&nbsp;becomes&nbsp;<span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode">&gt;</span> <span class="inlinecode">3</span>&nbsp;*)</span><br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;The&nbsp;same&nbsp;proof&nbsp;using&nbsp;<span class="inlinecode"><span class="id" type="var">false</span></span>:&nbsp;*)</span><br/>
&nbsp;&nbsp;- <span class="id" type="var">false</span> <span class="id" type="var">le_gt_false</span>. <span class="id" type="tactic">eauto</span>. <span class="id" type="tactic">eauto</span>.<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;The&nbsp;lemmas&nbsp;<span class="inlinecode"><span class="id" type="var">le_not_gt</span></span>&nbsp;and&nbsp;<span class="inlinecode"><span class="id" type="var">gt_not_le</span></span>&nbsp;work&nbsp;as&nbsp;well&nbsp;*)</span><br/>
&nbsp;&nbsp;- <span class="id" type="var">false</span> <span class="id" type="var">le_not_gt</span>. <span class="id" type="tactic">eauto</span>. <span class="id" type="tactic">eauto</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Abort</span>.<br/>
</div>

<div class="doc">
In the above example, <span class="inlinecode"><span class="id" type="var">false</span></span> <span class="inlinecode"><span class="id" type="var">le_gt_false</span>;</span> <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> proves the goal,
    but <span class="inlinecode"><span class="id" type="var">false</span></span> <span class="inlinecode"><span class="id" type="var">le_gt_false</span>;</span> <span class="inlinecode"><span class="id" type="tactic">auto</span></span> does not, because <span class="inlinecode"><span class="id" type="tactic">auto</span></span> does not
    correctly instantiate the existential variable. Note that <span class="inlinecode"><span class="id" type="var">false</span>*</span>
    <span class="inlinecode"><span class="id" type="var">le_gt_false</span></span> would not work either, because the star symbol tries
    to call <span class="inlinecode"><span class="id" type="tactic">auto</span></span> first. So, there are two possibilities for
    completing the proof: either call <span class="inlinecode"><span class="id" type="var">false</span></span> <span class="inlinecode"><span class="id" type="var">le_gt_false</span>;</span> <span class="inlinecode"><span class="id" type="tactic">eauto</span></span>, or
    call <span class="inlinecode"><span class="id" type="var">false</span>*</span> <span class="inlinecode">(<span class="id" type="var">le_gt_false</span></span> <span class="inlinecode">3)</span>. 
</div>

<div class="doc">
<a name="lab570"></a><h2 class="section">Automation for Transitivity Lemmas</h2>

<div class="paragraph"> </div>

 Some lemmas should never be added as hints, because they would
    very badly slow down proof search. The typical example is that of
    transitivity results. This section describes the problem and
    presents a general workaround.

<div class="paragraph"> </div>

    Consider a subtyping relation, written <span class="inlinecode"><span class="id" type="var">subtype</span></span> <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">T</span></span>, that relates
    two object <span class="inlinecode"><span class="id" type="var">S</span></span> and <span class="inlinecode"><span class="id" type="var">T</span></span> of type <span class="inlinecode"><span class="id" type="var">typ</span></span>. Assume that this relation
    has been proved reflexive and transitive. The corresponding lemmas
    are named <span class="inlinecode"><span class="id" type="var">subtype_refl</span></span> and <span class="inlinecode"><span class="id" type="var">subtype_trans</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Parameter</span> <span class="id" type="var">typ</span> : <span class="id" type="keyword">Type</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Parameter</span> <span class="id" type="var">subtype</span> : <span class="id" type="var">typ</span> → <span class="id" type="var">typ</span> → <span class="id" type="keyword">Prop</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Parameter</span> <span class="id" type="var">subtype_refl</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">T</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">subtype</span> <span class="id" type="var">T</span> <span class="id" type="var">T</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Parameter</span> <span class="id" type="var">subtype_trans</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">S</span> <span class="id" type="var">T</span> <span class="id" type="var">U</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">subtype</span> <span class="id" type="var">S</span> <span class="id" type="var">T</span> → <span class="id" type="var">subtype</span> <span class="id" type="var">T</span> <span class="id" type="var">U</span> → <span class="id" type="var">subtype</span> <span class="id" type="var">S</span> <span class="id" type="var">U</span>.<br/>
</div>

<div class="doc">
Adding reflexivity as hint is generally a good idea,
    so let's add reflexivity of subtyping as hint. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Hint</span> <span class="id" type="keyword">Resolve</span> <span class="id" type="var">subtype_refl</span>.<br/>
</div>

<div class="doc">
Adding transitivity as hint is generally a bad idea.  To
    understand why, let's add it as hint and see what happens.
    Because we cannot remove hints once we've added them, we are going
    to open a "Section," so as to restrict the scope of the
    transitivity hint to that section. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Section</span> <span class="id" type="var">HintsTransitivity</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Hint</span> <span class="id" type="keyword">Resolve</span> <span class="id" type="var">subtype_trans</span>.<br/>
</div>

<div class="doc">
Now, consider the goal <span class="inlinecode"><span style='font-size:120%;'>&forall;</span></span> <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">T</span>,</span> <span class="inlinecode"><span class="id" type="var">subtype</span></span> <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">T</span></span>, which clearly has
    no hope of being solved. Let's call <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> on this goal. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">transitivity_bad_hint_1</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">S</span> <span class="id" type="var">T</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">subtype</span> <span class="id" type="var">S</span> <span class="id" type="var">T</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span>. <span class="comment">(*&nbsp;debug&nbsp;*)</span> <span class="id" type="tactic">eauto</span>. <span class="comment">(*&nbsp;Investigates&nbsp;106&nbsp;applications...&nbsp;*)</span><br/>
<span class="id" type="keyword">Abort</span>.<br/>
</div>

<div class="doc">
Note that after closing the section, the hint <span class="inlinecode"><span class="id" type="var">subtype_trans</span></span>
    is no longer active. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">End</span> <span class="id" type="var">HintsTransitivity</span>.<br/>
</div>

<div class="doc">
In the previous example, the proof search has spent a lot of time
    trying to apply transitivity and reflexivity in every possible
    way.  Its process can be summarized as follows. The first goal is
    <span class="inlinecode"><span class="id" type="var">subtype</span></span> <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">T</span></span>. Since reflexivity does not apply, <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> invokes
    transitivity, which produces two subgoals, <span class="inlinecode"><span class="id" type="var">subtype</span></span> <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode">?<span class="id" type="var">X</span></span> and
    <span class="inlinecode"><span class="id" type="var">subtype</span></span> <span class="inlinecode">?<span class="id" type="var">X</span></span> <span class="inlinecode"><span class="id" type="var">T</span></span>. Solving the first subgoal, <span class="inlinecode"><span class="id" type="var">subtype</span></span> <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode">?<span class="id" type="var">X</span></span>, is
    straightforward, it suffices to apply reflexivity. This unifies
    <span class="inlinecode">?<span class="id" type="var">X</span></span> with <span class="inlinecode"><span class="id" type="var">S</span></span>. So, the second sugoal, <span class="inlinecode"><span class="id" type="var">subtype</span></span> <span class="inlinecode">?<span class="id" type="var">X</span></span> <span class="inlinecode"><span class="id" type="var">T</span></span>,
    becomes <span class="inlinecode"><span class="id" type="var">subtype</span></span> <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">T</span></span>, which is exactly what we started from...

<div class="paragraph"> </div>

    The problem with the transitivity lemma is that it is applicable
    to any goal concluding on a subtyping relation. Because of this,
    <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> keeps trying to apply it even though it most often doesn't
    help to solve the goal. So, one should never add a transitivity
    lemma as a hint for proof search. 
<div class="paragraph"> </div>

 There is a general workaround for having automation to exploit
    transitivity lemmas without giving up on efficiency. This workaround
    relies on a powerful mechanism called "external hint." This
    mechanism allows to manually describe the condition under which
    a particular lemma should be tried out during proof search.

<div class="paragraph"> </div>

    For the case of transitivity of subtyping, we are going to tell
    Coq to try and apply the transitivity lemma on a goal of the form
    <span class="inlinecode"><span class="id" type="var">subtype</span></span> <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">U</span></span> only when the proof context already contains an
    assumption either of the form <span class="inlinecode"><span class="id" type="var">subtype</span></span> <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">T</span></span> or of the form
    <span class="inlinecode"><span class="id" type="var">subtype</span></span> <span class="inlinecode"><span class="id" type="var">T</span></span> <span class="inlinecode"><span class="id" type="var">U</span></span>. In other words, we only apply the transitivity
    lemma when there is some evidence that this application might
    help.  To set up this "external hint," one has to write the
    following. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Hint</span> <span class="id" type="keyword">Extern</span> 1 (<span class="id" type="var">subtype</span> ?<span class="id" type="var">S</span> ?<span class="id" type="var">U</span>) ⇒<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">goal</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">H</span>: <span class="id" type="var">subtype</span> <span class="id" type="var">S</span> ?<span class="id" type="var">T</span> &#x22A2; <span class="id" type="var">_</span> ⇒ <span class="id" type="tactic">apply</span> (@<span class="id" type="var">subtype_trans</span> <span class="id" type="var">S</span> <span class="id" type="var">T</span> <span class="id" type="var">U</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">H</span>: <span class="id" type="var">subtype</span> ?<span class="id" type="var">T</span> <span class="id" type="var">U</span> &#x22A2; <span class="id" type="var">_</span> ⇒ <span class="id" type="tactic">apply</span> (@<span class="id" type="var">subtype_trans</span> <span class="id" type="var">S</span> <span class="id" type="var">T</span> <span class="id" type="var">U</span>)<br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/>
</div>

<div class="doc">
This hint declaration can be understood as follows.

<div class="paragraph"> </div>

<ul class="doclist">
<li> "Hint Extern" introduces the hint.

</li>
<li> The number "1" corresponds to a priority for proof search.
      It doesn't matter so much what priority is used in practice.

</li>
<li> The pattern <span class="inlinecode"><span class="id" type="var">subtype</span></span> <span class="inlinecode">?<span class="id" type="var">S</span></span> <span class="inlinecode">?<span class="id" type="var">U</span></span> describes the kind of goal on
      which the pattern should apply. The question marks are used
      to indicate that the variables <span class="inlinecode">?<span class="id" type="var">S</span></span> and <span class="inlinecode">?<span class="id" type="var">U</span></span> should be bound
      to some value in the rest of the hint description.

</li>
<li> The construction <span class="inlinecode"><span class="id" type="keyword">match</span></span> <span class="inlinecode"><span class="id" type="var">goal</span></span> <span class="inlinecode"><span class="id" type="keyword">with</span></span> <span class="inlinecode">...</span> <span class="inlinecode"><span class="id" type="keyword">end</span></span> tries to recognize
      patterns in the goal, or in the proof context, or both.

</li>
<li> The first pattern is <span class="inlinecode"><span class="id" type="var">H</span>:</span> <span class="inlinecode"><span class="id" type="var">subtype</span></span> <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode">?<span class="id" type="var">T</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">_</span></span>. It indices that
      the context should contain an hypothesis <span class="inlinecode"><span class="id" type="var">H</span></span> of type
      <span class="inlinecode"><span class="id" type="var">subtype</span></span> <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode">?<span class="id" type="var">T</span></span>, where <span class="inlinecode"><span class="id" type="var">S</span></span> has to be the same as in the goal,
      and where <span class="inlinecode">?<span class="id" type="var">T</span></span> can have any value.

</li>
<li> The symbol <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">_</span></span> at the end of <span class="inlinecode"><span class="id" type="var">H</span>:</span> <span class="inlinecode"><span class="id" type="var">subtype</span></span> <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode">?<span class="id" type="var">T</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" type="var">_</span></span> indicates
      that we do not impose further condition on how the proof
      obligation has to look like.

</li>
<li> The branch <span class="inlinecode">⇒</span> <span class="inlinecode"><span class="id" type="tactic">apply</span></span> <span class="inlinecode">(@<span class="id" type="var">subtype_trans</span></span> <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">T</span></span> <span class="inlinecode"><span class="id" type="var">U</span>)</span> that follows
      indicates that if the goal has the form <span class="inlinecode"><span class="id" type="var">subtype</span></span> <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">U</span></span> and if
      there exists an hypothesis of the form <span class="inlinecode"><span class="id" type="var">subtype</span></span> <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">T</span></span>, then
      we should try and apply transitivity lemma instantiated on
      the arguments <span class="inlinecode"><span class="id" type="var">S</span></span>, <span class="inlinecode"><span class="id" type="var">T</span></span> and <span class="inlinecode"><span class="id" type="var">U</span></span>. (Note: the symbol <span class="inlinecode">@</span> in front of
      <span class="inlinecode"><span class="id" type="var">subtype_trans</span></span> is only actually needed when the "Implicit Arguments"
      feature is activated.)

</li>
<li> The other branch, which corresponds to an hypothesis of the form
      <span class="inlinecode"><span class="id" type="var">H</span>:</span> <span class="inlinecode"><span class="id" type="var">subtype</span></span> <span class="inlinecode">?<span class="id" type="var">T</span></span> <span class="inlinecode"><span class="id" type="var">U</span></span> is symmetrical.

</li>
</ul>
    Note: the same external hint can be reused for any other transitive
    relation, simply by renaming <span class="inlinecode"><span class="id" type="var">subtype</span></span> into the name of that relation. 
<div class="paragraph"> </div>

 Let us see an example illustrating how the hint works. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">transitivity_workaround_1</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">T<sub>1</sub></span> <span class="id" type="var">T<sub>2</sub></span> <span class="id" type="var">T<sub>3</sub></span> <span class="id" type="var">T<sub>4</sub></span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">subtype</span> <span class="id" type="var">T<sub>1</sub></span> <span class="id" type="var">T<sub>2</sub></span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">subtype</span> <span class="id" type="var">T<sub>2</sub></span> <span class="id" type="var">T<sub>3</sub></span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">subtype</span> <span class="id" type="var">T<sub>3</sub></span> <span class="id" type="var">T<sub>4</sub></span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">subtype</span> <span class="id" type="var">T<sub>1</sub></span> <span class="id" type="var">T<sub>4</sub></span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span>. <span class="comment">(*&nbsp;debug&nbsp;*)</span> <span class="id" type="tactic">eauto</span>. <span class="comment">(*&nbsp;The&nbsp;trace&nbsp;shows&nbsp;the&nbsp;external&nbsp;hint&nbsp;being&nbsp;used&nbsp;*)</span><br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
We may also check that the new external hint does not suffer from the
    complexity blow up. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">transitivity_workaround_2</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">S</span> <span class="id" type="var">T</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">subtype</span> <span class="id" type="var">S</span> <span class="id" type="var">T</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span>. <span class="comment">(*&nbsp;debug&nbsp;*)</span> <span class="id" type="tactic">eauto</span>. <span class="comment">(*&nbsp;Investigates&nbsp;0&nbsp;applications&nbsp;*)</span><br/>
<span class="id" type="keyword">Abort</span>.<br/>
</div>

<div class="doc">
<a name="lab571"></a><h1 class="section">Decision Procedures</h1>

<div class="paragraph"> </div>

 A decision procedure is able to solve proof obligations whose
    statement admits a particular form. This section describes three
    useful decision procedures. The tactic <span class="inlinecode"><span class="id" type="tactic">omega</span></span> handles goals
    involving arithmetic and inequalities, but not general
    multiplications.  The tactic <span class="inlinecode"><span class="id" type="tactic">ring</span></span> handles goals involving
    arithmetic, including multiplications, but does not support
    inequalities. The tactic <span class="inlinecode"><span class="id" type="tactic">congruence</span></span> is able to prove equalities
    and inequalities by exploiting equalities available in the proof
    context. 
</div>

<div class="doc">
<a name="lab572"></a><h2 class="section">Omega</h2>

<div class="paragraph"> </div>

 The tactic <span class="inlinecode"><span class="id" type="tactic">omega</span></span> supports natural numbers (type <span class="inlinecode"><span class="id" type="var">nat</span></span>) as well as
    integers (type <span class="inlinecode"><span class="id" type="var">Z</span></span>, available by including the module <span class="inlinecode"><span class="id" type="var">ZArith</span></span>).
    It supports addition, substraction, equalities and inequalities.
    Before using <span class="inlinecode"><span class="id" type="tactic">omega</span></span>, one needs to import the module <span class="inlinecode"><span class="id" type="var">Omega</span></span>,
    as follows. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Omega</span>.<br/>
</div>

<div class="doc">
Here is an example. Let <span class="inlinecode"><span class="id" type="var">x</span></span> and <span class="inlinecode"><span class="id" type="var">y</span></span> be two natural numbers
    (they cannot be negative). Assume <span class="inlinecode"><span class="id" type="var">y</span></span> is less than 4, assume
    <span class="inlinecode"><span class="id" type="var">x</span>+<span class="id" type="var">x</span>+1</span> is less than <span class="inlinecode"><span class="id" type="var">y</span></span>, and assume <span class="inlinecode"><span class="id" type="var">x</span></span> is not zero. Then,
    it must be the case that <span class="inlinecode"><span class="id" type="var">x</span></span> is equal to one. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">omega_demo_1</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">x</span> <span class="id" type="var">y</span> : <span class="id" type="var">nat</span>),<br/>
&nbsp;&nbsp;(<span class="id" type="var">y</span> ≤ 4) →<br/>
&nbsp;&nbsp;(<span class="id" type="var">x</span> + <span class="id" type="var">x</span> + 1 ≤ <span class="id" type="var">y</span>) →<br/>
&nbsp;&nbsp;(<span class="id" type="var">x</span> ≠ 0) →<br/>
&nbsp;&nbsp;(<span class="id" type="var">x</span> = 1).<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">intros</span>. <span class="id" type="tactic">omega</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
Another example: if <span class="inlinecode"><span class="id" type="var">z</span></span> is the mean of <span class="inlinecode"><span class="id" type="var">x</span></span> and <span class="inlinecode"><span class="id" type="var">y</span></span>, and if the
    difference between <span class="inlinecode"><span class="id" type="var">x</span></span> and <span class="inlinecode"><span class="id" type="var">y</span></span> is at most <span class="inlinecode">4</span>, then the difference
    between <span class="inlinecode"><span class="id" type="var">x</span></span> and <span class="inlinecode"><span class="id" type="var">z</span></span> is at most 2. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">omega_demo_2</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">x</span> <span class="id" type="var">y</span> <span class="id" type="var">z</span> : <span class="id" type="var">nat</span>),<br/>
&nbsp;&nbsp;(<span class="id" type="var">x</span> + <span class="id" type="var">y</span> = <span class="id" type="var">z</span> + <span class="id" type="var">z</span>) →<br/>
&nbsp;&nbsp;(<span class="id" type="var">x</span> - <span class="id" type="var">y</span> ≤ 4) →<br/>
&nbsp;&nbsp;(<span class="id" type="var">x</span> - <span class="id" type="var">z</span> ≤ 2).<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">intros</span>. <span class="id" type="tactic">omega</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
One can proof <span class="inlinecode"><span class="id" type="var">False</span></span> using <span class="inlinecode"><span class="id" type="tactic">omega</span></span> if the mathematical facts
    from the context are contradictory. In the following example,
    the constraints on the values <span class="inlinecode"><span class="id" type="var">x</span></span> and <span class="inlinecode"><span class="id" type="var">y</span></span> cannot be all
    satisfied in the same time. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">omega_demo_3</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">x</span> <span class="id" type="var">y</span> : <span class="id" type="var">nat</span>),<br/>
&nbsp;&nbsp;(<span class="id" type="var">x</span> + 5 ≤ <span class="id" type="var">y</span>) →<br/>
&nbsp;&nbsp;(<span class="id" type="var">y</span> - <span class="id" type="var">x</span> &lt; 3) →<br/>
&nbsp;&nbsp;<span class="id" type="var">False</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">intros</span>. <span class="id" type="tactic">omega</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
Note: <span class="inlinecode"><span class="id" type="tactic">omega</span></span> can prove a goal by contradiction only if its
    conclusion reduces to <span class="inlinecode"><span class="id" type="var">False</span></span>. The tactic <span class="inlinecode"><span class="id" type="tactic">omega</span></span> always fails
    when the conclusion is an arbitrary proposition <span class="inlinecode"><span class="id" type="var">P</span></span>, even though
    <span class="inlinecode"><span class="id" type="var">False</span></span> implies any proposition <span class="inlinecode"><span class="id" type="var">P</span></span> (by <span class="inlinecode"><span class="id" type="var">ex_falso_quodlibet</span></span>). 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">omega_demo_4</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">x</span> <span class="id" type="var">y</span> : <span class="id" type="var">nat</span>) (<span class="id" type="var">P</span> : <span class="id" type="keyword">Prop</span>),<br/>
&nbsp;&nbsp;(<span class="id" type="var">x</span> + 5 ≤ <span class="id" type="var">y</span>) →<br/>
&nbsp;&nbsp;(<span class="id" type="var">y</span> - <span class="id" type="var">x</span> &lt; 3) →<br/>
&nbsp;&nbsp;<span class="id" type="var">P</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;Calling&nbsp;<span class="inlinecode"><span class="id" type="tactic">omega</span></span>&nbsp;at&nbsp;this&nbsp;point&nbsp;fails&nbsp;with&nbsp;the&nbsp;message:<br/>
&nbsp;&nbsp;&nbsp;&nbsp;"Omega:&nbsp;Can't&nbsp;solve&nbsp;a&nbsp;goal&nbsp;with&nbsp;proposition&nbsp;variables"&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;So,&nbsp;one&nbsp;needs&nbsp;to&nbsp;replace&nbsp;the&nbsp;goal&nbsp;by&nbsp;<span class="inlinecode"><span class="id" type="var">False</span></span>&nbsp;first.&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="var">false</span>. <span class="id" type="tactic">omega</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab573"></a><h2 class="section">Ring</h2>

<div class="paragraph"> </div>

 Compared with <span class="inlinecode"><span class="id" type="tactic">omega</span></span>, the tactic <span class="inlinecode"><span class="id" type="tactic">ring</span></span> adds support for
    multiplications, however it gives up the ability to reason on
    inequations. Moreover, it supports only integers (type <span class="inlinecode"><span class="id" type="var">Z</span></span>) and
    not natural numbers (type <span class="inlinecode"><span class="id" type="var">nat</span></span>). Here is an example showing how
    to use <span class="inlinecode"><span class="id" type="tactic">ring</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">ZArith</span>.<br/>
<span class="id" type="keyword">Module</span> <span class="id" type="var">RingDemo</span>.<br/>
&nbsp;&nbsp;<span class="id" type="keyword">Open</span> <span class="id" type="keyword">Scope</span> <span class="id" type="var">Z_scope</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;Arithmetic&nbsp;symbols&nbsp;are&nbsp;now&nbsp;interpreted&nbsp;in&nbsp;<span class="inlinecode"><span class="id" type="var">Z</span></span>&nbsp;*)</span><br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">ring_demo</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">x</span> <span class="id" type="var">y</span> <span class="id" type="var">z</span> : <span class="id" type="var">Z</span>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">x</span> * (<span class="id" type="var">y</span> + <span class="id" type="var">z</span>) - <span class="id" type="var">z</span> * 3 * <span class="id" type="var">x</span><br/>
&nbsp;&nbsp;= <span class="id" type="var">x</span> * <span class="id" type="var">y</span> - 2 * <span class="id" type="var">x</span> * <span class="id" type="var">z</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">intros</span>. <span class="id" type="tactic">ring</span>. <span class="id" type="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">End</span> <span class="id" type="var">RingDemo</span>.<br/>
</div>

<div class="doc">
<a name="lab574"></a><h2 class="section">Congruence</h2>

<div class="paragraph"> </div>

 The tactic <span class="inlinecode"><span class="id" type="tactic">congruence</span></span> is able to exploit equalities from the
    proof context in order to automatically perform the rewriting
    operations necessary to establish a goal. It is slightly more
    powerful than the tactic <span class="inlinecode"><span class="id" type="tactic">subst</span></span>, which can only handle equalities
    of the form <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">e</span></span> where <span class="inlinecode"><span class="id" type="var">x</span></span> is a variable and <span class="inlinecode"><span class="id" type="var">e</span></span> an
    expression. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">congruence_demo_1</span> :<br/>
&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">f</span> : <span class="id" type="var">nat</span>→<span class="id" type="var">nat</span>→<span class="id" type="var">nat</span>) (<span class="id" type="var">g</span> <span class="id" type="var">h</span> : <span class="id" type="var">nat</span>→<span class="id" type="var">nat</span>) (<span class="id" type="var">x</span> <span class="id" type="var">y</span> <span class="id" type="var">z</span> : <span class="id" type="var">nat</span>),<br/>
&nbsp;&nbsp;&nbsp;<span class="id" type="var">f</span> (<span class="id" type="var">g</span> <span class="id" type="var">x</span>) (<span class="id" type="var">g</span> <span class="id" type="var">y</span>) = <span class="id" type="var">z</span> →<br/>
&nbsp;&nbsp;&nbsp;2 = <span class="id" type="var">g</span> <span class="id" type="var">x</span> →<br/>
&nbsp;&nbsp;&nbsp;<span class="id" type="var">g</span> <span class="id" type="var">y</span> = <span class="id" type="var">h</span> <span class="id" type="var">z</span> →<br/>
&nbsp;&nbsp;&nbsp;<span class="id" type="var">f</span> 2 (<span class="id" type="var">h</span> <span class="id" type="var">z</span>) = <span class="id" type="var">z</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">intros</span>. <span class="id" type="tactic">congruence</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
Moreover, <span class="inlinecode"><span class="id" type="tactic">congruence</span></span> is able to exploit universally quantified
    equalities, for example <span class="inlinecode"><span style='font-size:120%;'>&forall;</span></span> <span class="inlinecode"><span class="id" type="var">a</span>,</span> <span class="inlinecode"><span class="id" type="var">g</span></span> <span class="inlinecode"><span class="id" type="var">a</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">h</span></span> <span class="inlinecode"><span class="id" type="var">a</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">congruence_demo_2</span> :<br/>
&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">f</span> : <span class="id" type="var">nat</span>→<span class="id" type="var">nat</span>→<span class="id" type="var">nat</span>) (<span class="id" type="var">g</span> <span class="id" type="var">h</span> : <span class="id" type="var">nat</span>→<span class="id" type="var">nat</span>) (<span class="id" type="var">x</span> <span class="id" type="var">y</span> <span class="id" type="var">z</span> : <span class="id" type="var">nat</span>),<br/>
&nbsp;&nbsp;&nbsp;(<span style='font-size:120%;'>&forall;</span><span class="id" type="var">a</span>, <span class="id" type="var">g</span> <span class="id" type="var">a</span> = <span class="id" type="var">h</span> <span class="id" type="var">a</span>) →<br/>
&nbsp;&nbsp;&nbsp;<span class="id" type="var">f</span> (<span class="id" type="var">g</span> <span class="id" type="var">x</span>) (<span class="id" type="var">g</span> <span class="id" type="var">y</span>) = <span class="id" type="var">z</span> →<br/>
&nbsp;&nbsp;&nbsp;<span class="id" type="var">g</span> <span class="id" type="var">x</span> = 2 →<br/>
&nbsp;&nbsp;&nbsp;<span class="id" type="var">f</span> 2 (<span class="id" type="var">h</span> <span class="id" type="var">y</span>) = <span class="id" type="var">z</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">congruence</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
Next is an example where <span class="inlinecode"><span class="id" type="tactic">congruence</span></span> is very useful. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">congruence_demo_4</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">f</span> <span class="id" type="var">g</span> : <span class="id" type="var">nat</span>→<span class="id" type="var">nat</span>),<br/>
&nbsp;&nbsp;(<span style='font-size:120%;'>&forall;</span><span class="id" type="var">a</span>, <span class="id" type="var">f</span> <span class="id" type="var">a</span> = <span class="id" type="var">g</span> <span class="id" type="var">a</span>) →<br/>
&nbsp;&nbsp;<span class="id" type="var">f</span> (<span class="id" type="var">g</span> (<span class="id" type="var">g</span> 2)) = <span class="id" type="var">g</span> (<span class="id" type="var">f</span> (<span class="id" type="var">f</span> 2)).<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">congruence</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
The tactic <span class="inlinecode"><span class="id" type="tactic">congruence</span></span> is able to prove a contradiction if the
    goal entails an equality that contradicts an inequality available
    in the proof context. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">congruence_demo_3</span> :<br/>
&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">f</span> <span class="id" type="var">g</span> <span class="id" type="var">h</span> : <span class="id" type="var">nat</span>→<span class="id" type="var">nat</span>) (<span class="id" type="var">x</span> : <span class="id" type="var">nat</span>),<br/>
&nbsp;&nbsp;&nbsp;(<span style='font-size:120%;'>&forall;</span><span class="id" type="var">a</span>, <span class="id" type="var">f</span> <span class="id" type="var">a</span> = <span class="id" type="var">h</span> <span class="id" type="var">a</span>) →<br/>
&nbsp;&nbsp;&nbsp;<span class="id" type="var">g</span> <span class="id" type="var">x</span> = <span class="id" type="var">f</span> <span class="id" type="var">x</span> →<br/>
&nbsp;&nbsp;&nbsp;<span class="id" type="var">g</span> <span class="id" type="var">x</span> ≠ <span class="id" type="var">h</span> <span class="id" type="var">x</span> →<br/>
&nbsp;&nbsp;&nbsp;<span class="id" type="var">False</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">congruence</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
One of the strengths of <span class="inlinecode"><span class="id" type="tactic">congruence</span></span> is that it is a very fast
    tactic. So, one should not hesitate to invoke it wherever it might
    help. 
</div>

<div class="doc">
<a name="lab575"></a><h1 class="section">Summary</h1>

<div class="paragraph"> </div>

 Let us summarize the main automation tactics available.

<div class="paragraph"> </div>

<ul class="doclist">
<li> <span class="inlinecode"><span class="id" type="tactic">auto</span></span> automatically applies <span class="inlinecode"><span class="id" type="tactic">reflexivity</span></span>, <span class="inlinecode"><span class="id" type="tactic">assumption</span></span>, and <span class="inlinecode"><span class="id" type="tactic">apply</span></span>.

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> moreover tries <span class="inlinecode"><span class="id" type="tactic">eapply</span></span>, and in particular can instantiate
      existentials in the conclusion.

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" type="var">iauto</span></span> extends <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> with support for negation, conjunctions, and
      disjunctions. However, its support for disjunction can make it
      exponentially slow.

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" type="var">jauto</span></span> extends <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> with support for  negation, conjunctions, and
      existential at the head of hypothesis.

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" type="tactic">congruence</span></span> helps reasoning about equalities and inequalities.

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" type="tactic">omega</span></span> proves arithmetic goals with equalities and inequalities,
      but it does not support multiplication.

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" type="tactic">ring</span></span> proves arithmetic goals with multiplications, but does not
      support inequalities.

</li>
</ul>
    In order to set up automation appropriately, keep in mind the following
    rule of thumbs:

<div class="paragraph"> </div>

<ul class="doclist">
<li> automation is all about balance: not enough automation makes proofs
      not very robust on change, whereas too much automation makes proofs
      very hard to fix when they break.

<div class="paragraph"> </div>


</li>
<li> if a lemma is not goal directed (i.e., some of its variables do not
      occur in its conclusion), then the premises need to be ordered in
      such a way that proving the first premises maximizes the chances of
      correctly instantiating the variables that do not occur in the conclusion.

<div class="paragraph"> </div>


</li>
<li> a lemma whose conclusion is <span class="inlinecode"><span class="id" type="var">False</span></span> should only be added as a local
      hint, i.e., as a hint within the current section.

<div class="paragraph"> </div>


</li>
<li> a transitivity lemma should never be considered as hint; if automation
      of transitivity reasoning is really necessary, an <span class="inlinecode"><span class="id" type="keyword">Extern</span></span> <span class="inlinecode"><span class="id" type="keyword">Hint</span></span> needs
      to be set up.

<div class="paragraph"> </div>


</li>
<li> a definition usually needs to be accompanied with a <span class="inlinecode"><span class="id" type="keyword">Hint</span></span> <span class="inlinecode"><span class="id" type="keyword">Unfold</span></span>.

</li>
</ul>
    Becoming a master in the black art of automation certainly requires
    some investment, however this investment will pay off very quickly.

</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;Thu&nbsp;Feb&nbsp;7&nbsp;20:09:27&nbsp;EST&nbsp;2019&nbsp;*)</span><br/>
</div>
</div>



</div>

</body>
</html>